let P be Instruction-Sequence of SCMPDS; 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 ; 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; 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; ( 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) )
; 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
; verum