let P be Instruction-Sequence of SCMPDS; :: thesis: for I, J being Program of SCMPDS
for s being 0 -started 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)),s) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,k)))
let I, J be Program of SCMPDS; :: thesis: for s being 0 -started 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)),s) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,k)))
let s be 0 -started 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)),s) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),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)),s) implies CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,k))) )
set P1 = P +* (stop I);
set P2 = P +* (stop (I ';' J));
set s3 = Comput ((P +* (stop I)),s,k);
set s4 = Comput ((P +* (stop (I ';' J))),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)),s) ) ; :: thesis: CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,k)))
I: Initialize s = s by MEMSTR_0:44;
then A5: IC (Comput ((P +* (stop I)),s,k)) in dom I by A3, A4, Th40;
A6: IC (Comput ((P +* (stop I)),s,k)) = IC (Comput ((P +* (stop (I ';' J))),s,k)) by A3, A4, Th39;
A7: IC (Comput ((P +* (stop I)),s,k)) in dom (stop I) by A3, Def2, I;
A8: ( dom (stop I) c= dom (stop (I ';' J)) & stop (I ';' J) c= P +* (stop (I ';' J)) ) by FUNCT_4:25, SCMPDS_5:13;
A9: stop I c= P +* (stop I) by FUNCT_4:25;
A10: stop (I ';' J) = (I ';' J) ';' (Stop SCMPDS)
.= I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:27 ;
A11: (P +* (stop I)) /. (IC (Comput ((P +* (stop I)),s,k))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,k))) by PBOOLE:143;
A12: (P +* (stop (I ';' J))) /. (IC (Comput ((P +* (stop (I ';' J))),s,k))) = (P +* (stop (I ';' J))) . (IC (Comput ((P +* (stop (I ';' J))),s,k))) by PBOOLE:143;
thus CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,k))) by A11
.= (stop I) . (IC (Comput ((P +* (stop I)),s,k))) by A7, A9, GRFUNC_1:2
.= I . (IC (Comput ((P +* (stop I)),s,k))) by A5, AFINSQ_1:def 3
.= (stop (I ';' J)) . (IC (Comput ((P +* (stop I)),s,k))) by A5, A10, AFINSQ_1:def 3
.= (P +* (stop (I ';' J))) . (IC (Comput ((P +* (stop (I ';' J))),s,k))) by A6, A7, A8, GRFUNC_1:2
.= CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,k))) by A12 ; :: thesis: verum