let a be Int_position; :: thesis: for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free parahalting Program of

for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS

for I being halt-free parahalting Program of

for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free parahalting Program of

for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

let I be halt-free parahalting Program of ; :: thesis: for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

let j be shiftable parahalting Instruction of SCMPDS; :: thesis: (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

set Mj = Load j;

set SA = Start-At (((IC (IExec ((Load j),P,(Initialize (IExec (I,P,s)))))) + (card I)),SCMPDS);

A1: not a in dom (Start-At (((IC (IExec ((Load j),P,(Initialize (IExec (I,P,s)))))) + (card I)),SCMPDS)) by SCMPDS_4:18;

A2: a in SCM-Data-Loc by AMI_2:def 16;

for a being Int_position holds (Initialize (IExec (I,P,s))) . a = (IExec (I,P,s)) . a by Th4;

then A3: DataPart (Initialize (IExec (I,P,s))) = DataPart (IExec (I,P,s)) by SCMPDS_4:8;

thus (IExec ((I ';' j),P,s)) . a = (IncIC ((IExec ((Load j),P,(Initialize (IExec (I,P,s))))),(card I))) . a by Th22

.= (IExec ((Load j),P,(Initialize (IExec (I,P,s))))) . a by A1, FUNCT_4:11

.= (Exec (j,(Initialize (IExec (I,P,s))))) . a by Th27

.= (DataPart (Exec (j,(Initialize (IExec (I,P,s)))))) . a by A2, FUNCT_1:49, SCMPDS_2:84

.= (DataPart (Exec (j,(IExec (I,P,s))))) . a by A3, Th26

.= (Exec (j,(IExec (I,P,s)))) . a by A2, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum

for s being 0 -started State of SCMPDS

for I being halt-free parahalting Program of

for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS

for I being halt-free parahalting Program of

for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free parahalting Program of

for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

let I be halt-free parahalting Program of ; :: thesis: for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

let j be shiftable parahalting Instruction of SCMPDS; :: thesis: (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

set Mj = Load j;

set SA = Start-At (((IC (IExec ((Load j),P,(Initialize (IExec (I,P,s)))))) + (card I)),SCMPDS);

A1: not a in dom (Start-At (((IC (IExec ((Load j),P,(Initialize (IExec (I,P,s)))))) + (card I)),SCMPDS)) by SCMPDS_4:18;

A2: a in SCM-Data-Loc by AMI_2:def 16;

for a being Int_position holds (Initialize (IExec (I,P,s))) . a = (IExec (I,P,s)) . a by Th4;

then A3: DataPart (Initialize (IExec (I,P,s))) = DataPart (IExec (I,P,s)) by SCMPDS_4:8;

thus (IExec ((I ';' j),P,s)) . a = (IncIC ((IExec ((Load j),P,(Initialize (IExec (I,P,s))))),(card I))) . a by Th22

.= (IExec ((Load j),P,(Initialize (IExec (I,P,s))))) . a by A1, FUNCT_4:11

.= (Exec (j,(Initialize (IExec (I,P,s))))) . a by Th27

.= (DataPart (Exec (j,(Initialize (IExec (I,P,s)))))) . a by A2, FUNCT_1:49, SCMPDS_2:84

.= (DataPart (Exec (j,(IExec (I,P,s))))) . a by A3, Th26

.= (Exec (j,(IExec (I,P,s)))) . a by A2, FUNCT_1:49, SCMPDS_2:84 ; :: thesis: verum