let I, J be Program of SCMPDS; for s being State of SCMPDS
for k being Element of NAT st I is_closed_on s & I is_halting_on s & k < LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) holds
CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) = CurInstr ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)))
let s be State of SCMPDS; for k being Element of NAT st I is_closed_on s & I is_halting_on s & k < LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) holds
CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) = CurInstr ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)))
let k be Element of NAT ; ( I is_closed_on s & I is_halting_on s & k < LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) implies CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) = CurInstr ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k))) )
set s1 = (Initialize s) +* (stop I);
set s2 = (Initialize s) +* (stop (I ';' J));
set s3 = Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k);
set s4 = Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k);
set SS = Stop SCMPDS;
A1:
s +* (Initialize (stop I)) = (Initialize s) +* (stop I)
by COMPOS_1:125;
A2:
s +* (Initialize (stop (I ';' J))) = (Initialize s) +* (stop (I ';' J))
by COMPOS_1:125;
assume that
A3:
I is_closed_on s
and
A4:
( I is_halting_on s & k < LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) )
; CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) = CurInstr ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)))
A5:
IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) in dom I
by A3, A4, Th40;
A6:
IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) = IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k))
by A3, A4, Th39;
A7:
IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) in dom (stop I)
by A3, Def2;
( Initialize (stop (I ';' J)) c= (Initialize s) +* (stop (I ';' J)) & stop (I ';' J) c= Initialize (stop (I ';' J)) )
by A2, COMPOS_1:126, FUNCT_4:26;
then A8:
( dom (stop I) c= dom (stop (I ';' J)) & stop (I ';' J) c= (Initialize s) +* (stop (I ';' J)) )
by SCMPDS_5:16, XBOOLE_1:1;
( Initialize (stop I) c= (Initialize s) +* (stop I) & stop I c= Initialize (stop I) )
by A1, COMPOS_1:126, FUNCT_4:26;
then A9:
stop I c= (Initialize s) +* (stop I)
by XBOOLE_1:1;
A10: stop (I ';' J) =
(I ';' J) ';' (Stop SCMPDS)
.=
I ';' (J ';' (Stop SCMPDS))
by AFINSQ_1:30
;
A11:
(ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) = (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)))
by COMPOS_1:38;
A12:
(ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k))) = (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)))
by COMPOS_1:38;
A13:
ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))
by AMI_1:123;
A14:
ProgramPart ((Initialize s) +* (stop (I ';' J))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k))
by AMI_1:123;
thus CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k))) =
((Initialize s) +* (stop I)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)))
by A11, A13, AMI_1:54
.=
(stop I) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)))
by A7, A9, GRFUNC_1:8
.=
I . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)))
by A5, AFINSQ_1:def 4
.=
(stop (I ';' J)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)))
by A5, A10, AFINSQ_1:def 4
.=
((Initialize s) +* (stop (I ';' J))) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)))
by A6, A7, A8, GRFUNC_1:8
.=
CurInstr ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)))
by A12, A14, AMI_1:54
; verum