let a be Int_position ; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),s)) . a = (Exec (j,(IExec (I,s)))) . a
let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free parahalting Program of SCMPDS
for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),s)) . a = (Exec (j,(IExec (I,s)))) . a
let I be halt-free parahalting Program of SCMPDS; :: thesis: for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),s)) . a = (Exec (j,(IExec (I,s)))) . a
let j be shiftable parahalting Instruction of SCMPDS; :: thesis: (IExec ((I ';' j),s)) . a = (Exec (j,(IExec (I,s)))) . a
set Mj = Load j;
set SA = Start-At (((IC (IExec ((Load j),(IExec (I,s))))) + (card I)),SCMPDS);
A1: not a in dom (Start-At (((IC (IExec ((Load j),(IExec (I,s))))) + (card I)),SCMPDS)) by SCMPDS_4:59;
A2: a in SCM-Data-Loc by SCMPDS_2:def 2;
for a being Int_position holds (Initialize (IExec (I,s))) . a = (IExec (I,s)) . a by Th40;
then A3: DataPart (Initialize (IExec (I,s))) = DataPart (IExec (I,s)) by SCMPDS_4:23;
thus (IExec ((I ';' j),s)) . a = ((IExec ((Load j),(IExec (I,s)))) +* (Start-At (((IC (IExec ((Load j),(IExec (I,s))))) + (card I)),SCMPDS))) . a by Th38
.= (IExec ((Load j),(IExec (I,s)))) . a by A1, FUNCT_4:12
.= (Exec (j,(Initialize (IExec (I,s))))) . a by Th45
.= (DataPart (Exec (j,(Initialize (IExec (I,s)))))) . a by A2, FUNCT_1:72, SCMPDS_2:100
.= (DataPart (Exec (j,(IExec (I,s))))) . a by A3, Th44
.= (Exec (j,(IExec (I,s)))) . a by A2, FUNCT_1:72, SCMPDS_2:100 ; :: thesis: verum