let a be Int_position ; :: thesis: for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being halt-free Program of SCMPDS
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 State of SCMPDS; :: thesis: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being halt-free Program of SCMPDS
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 the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for I being halt-free Program of SCMPDS
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 SCMPDS; :: 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
set Mj = Load j;
A3: a in SCM-Data-Loc by SCMPDS_2:def 2;
for a being Int_position holds (Initialize (IExec (I,P,s))) . a = (IExec (I,P,s)) . a by SCMPDS_5:40;
then A4: DataPart (Initialize (IExec (I,P,s))) = DataPart (IExec (I,P,s)) by SCMPDS_4:23;
A5: Load j is_halting_on IExec (I,P,s),P by SCMPDS_6:35;
Load j is_closed_on IExec (I,P,s),P by SCMPDS_6:34;
hence (IExec ((I ';' j),P,s)) . a = (IExec ((Load j),P,(IExec (I,P,s)))) . a by A1, A2, A5, Th49
.= (Exec (j,(Initialize (IExec (I,P,s))))) . a by SCMPDS_5:45
.= (DataPart (Exec (j,(Initialize (IExec (I,P,s)))))) . a by A3, FUNCT_1:72, SCMPDS_2:100
.= (DataPart (Exec (j,(IExec (I,P,s))))) . a by A4, SCMPDS_5:44
.= (Exec (j,(IExec (I,P,s)))) . a by A3, FUNCT_1:72, SCMPDS_2:100 ;
:: thesis: verum