let a be Int_position ; :: thesis: for s being State of SCMPDS
for i being No-StopCode parahalting Instruction of SCMPDS
for j being shiftable parahalting Instruction of SCMPDS holds (IExec (i ';' j),s) . a = (Exec j,(Exec i,(Initialize s))) . a
let s be State of SCMPDS ; :: thesis: for i being No-StopCode parahalting Instruction of SCMPDS
for j being shiftable parahalting Instruction of SCMPDS holds (IExec (i ';' j),s) . a = (Exec j,(Exec i,(Initialize s))) . a
let i be No-StopCode parahalting Instruction of SCMPDS ; :: thesis: for j being shiftable parahalting Instruction of SCMPDS holds (IExec (i ';' j),s) . a = (Exec j,(Exec i,(Initialize s))) . a
let j be shiftable parahalting Instruction of SCMPDS ; :: thesis: (IExec (i ';' j),s) . a = (Exec j,(Exec i,(Initialize s))) . a
set Mi = Load i;
thus (IExec (i ';' j),s) . a = (IExec ((Load i) ';' j),s) . a
.= (Exec j,(IExec (Load i),s)) . a by Th46
.= (Exec j,(Exec i,(Initialize s))) . a by Th45 ; :: thesis: verum