let P be Instruction-Sequence of SCMPDS; :: thesis: for I, J being Program of
for s being 0 -started State of SCMPDS
for k being 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 ; :: thesis: for s being 0 -started State of SCMPDS
for k being 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 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 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
A1: I is_closed_on s,P and
A2: ( 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)))
A3: Initialize s = s by MEMSTR_0:44;
then A4: IC (Comput ((P +* (stop I)),s,k)) in dom I by A1, A2, Th17;
A5: IC (Comput ((P +* (stop I)),s,k)) = IC (Comput ((P +* (stop (I ';' J))),s,k)) by A1, A2, Th16;
A6: IC (Comput ((P +* (stop I)),s,k)) in dom (stop I) by A1, A3;
A7: ( dom (stop I) c= dom (stop (I ';' J)) & stop (I ';' J) c= P +* (stop (I ';' J)) ) by FUNCT_4:25, SCMPDS_5:13;
A8: stop I c= P +* (stop I) by FUNCT_4:25;
A9: stop (I ';' J) = (I ';' J) ';' (Stop SCMPDS)
.= I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:27 ;
A10: (P +* (stop I)) /. (IC (Comput ((P +* (stop I)),s,k))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,k))) by PBOOLE:143;
A11: (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 A10
.= (stop I) . (IC (Comput ((P +* (stop I)),s,k))) by A6, A8, GRFUNC_1:2
.= I . (IC (Comput ((P +* (stop I)),s,k))) by A4, AFINSQ_1:def 3
.= (stop (I ';' J)) . (IC (Comput ((P +* (stop I)),s,k))) by A4, A9, AFINSQ_1:def 3
.= (P +* (stop (I ';' J))) . (IC (Comput ((P +* (stop (I ';' J))),s,k))) by A5, A6, A7, GRFUNC_1:2
.= CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,k))) by A11 ; :: thesis: verum