let s be State of SCMPDS ; :: thesis: for i being No-StopCode parahalting Instruction of SCMPDS
for J being parahalting shiftable Program of SCMPDS
for a being Int_position holds (IExec (i ';' J),s) . a = (IExec J,(Exec i,(Initialize s))) . a
let i be No-StopCode parahalting Instruction of SCMPDS ; :: thesis: for J being parahalting shiftable Program of SCMPDS
for a being Int_position holds (IExec (i ';' J),s) . a = (IExec J,(Exec i,(Initialize s))) . a
let J be parahalting shiftable Program of SCMPDS ; :: thesis: for a being Int_position holds (IExec (i ';' J),s) . a = (IExec J,(Exec i,(Initialize s))) . a
let a be Int_position ; :: thesis: (IExec (i ';' J),s) . a = (IExec J,(Exec i,(Initialize s))) . a
thus (IExec (i ';' J),s) . a = (IExec ((Load i) ';' J),s) . a
.= (IExec J,(IExec (Load i),s)) . a by SCMPDS_5:39
.= (IExec J,(Exec i,(Initialize s))) . a by SCMPDS_5:45 ; :: thesis: verum