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