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 Program of
for j being shiftable parahalting Instruction of SCMPDS st I is_closed_on s,P & I is_halting_on s,P 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 Program of
for j being shiftable parahalting Instruction of SCMPDS st I is_closed_on s,P & I is_halting_on s,P 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 Program of
for j being shiftable parahalting Instruction of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
(IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

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

let j be shiftable parahalting Instruction of SCMPDS; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a )
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P ; :: thesis: (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a