let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for I, J being Program of SCMPDS
for s being State of SCMPDS
for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),k)))
let I, J be Program of SCMPDS; :: thesis: for s being State of SCMPDS
for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),k)))
let s be State of SCMPDS; :: thesis: for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),k)))
let k be Element of NAT ; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) implies CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),k))) )
set s1 = Initialize s;
set s2 = Initialize s;
set P1 = P +* (stop I);
set P2 = P +* (stop (I ';' J));
set s3 = Comput ((P +* (stop I)),(Initialize s),k);
set s4 = Comput ((P +* (stop (I ';' J))),(Initialize s),k);
set P3 = P +* (stop I);
set P4 = P +* (stop (I ';' J));
set SS = Stop SCMPDS;
assume that
A3: I is_closed_on s,P and
A4: ( I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) ) ; :: thesis: CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),k)))
A5: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I by A3, A4, Th40;
A6: IC (Comput ((P +* (stop I)),(Initialize s),k)) = IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) by A3, A4, Th39;
A7: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) by A3, Def2;
A8: ( dom (stop I) c= dom (stop (I ';' J)) & stop (I ';' J) c= P +* (stop (I ';' J)) ) by SCMPDS_5:16, FUNCT_4:26;
A9: stop I c= P +* (stop I) by FUNCT_4:26;
A10: stop (I ';' J) = (I ';' J) ';' (Stop SCMPDS)
.= I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:30 ;
A11: (P +* (stop I)) /. (IC (Comput ((P +* (stop I)),(Initialize s),k))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by PBOOLE:158;
A12: (P +* (stop (I ';' J))) /. (IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k))) = (P +* (stop (I ';' J))) . (IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k))) by PBOOLE:158;
thus CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A11
.= (stop I) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A7, A9, GRFUNC_1:8
.= I . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A5, AFINSQ_1:def 4
.= (stop (I ';' J)) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A5, A10, AFINSQ_1:def 4
.= (P +* (stop (I ';' J))) . (IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k))) by A6, A7, A8, GRFUNC_1:8
.= CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),k))) by A12 ; :: thesis: verum