set WHL = while<>0 (F4(),F5(),F3());
set s1 = (Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())));
set ps = ProgramPart F2();
A6:
(Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))) = F2() +* (Initialize (stop (while<>0 (F4(),F5(),F3()))))
by COMPOS_1:125;
set sI = (Initialize F2()) +* (stop F3());
set m1 = (LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 2;
set s2 = (Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())));
set m2 = LifeSpan ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))));
A7:
(Initialize F2()) +* (stop F3()) = F2() +* (Initialize (stop F3()))
by COMPOS_1:125;
A8:
(Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))) = (IExec (F3(),F2())) +* (Initialize (stop (while<>0 (F4(),F5(),F3()))))
by COMPOS_1:125;
A9:
Initialize (stop F3()) c= (Initialize F2()) +* (stop F3())
by A7, FUNCT_4:26;
F3() is_closed_on F2()
by A2, A4, A5;
then A10:
F3() is_closed_on (Initialize F2()) +* (stop F3())
by SCMPDS_6:38;
F3() is_halting_on F2()
by A2, A4, A5;
then A11:
ProgramPart ((Initialize F2()) +* (stop F3())) halts_on (Initialize F2()) +* (stop F3())
by SCMPDS_6:def 3;
A12:
(Initialize ((Initialize F2()) +* (stop F3()))) +* (stop F3()) = ((Initialize F2()) +* (stop F3())) +* (Initialize (stop F3()))
by COMPOS_1:125;
(Initialize F2()) +* (stop F3()) = (Initialize ((Initialize F2()) +* (stop F3()))) +* (stop F3())
by A9, A12, FUNCT_4:79;
then
ProgramPart ((Initialize ((Initialize F2()) +* (stop F3()))) +* (stop F3())) halts_on (Initialize ((Initialize F2()) +* (stop F3()))) +* (stop F3())
by A11;
then A13:
F3() is_halting_on (Initialize F2()) +* (stop F3())
by SCMPDS_6:def 3;
set s4 = Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1);
set i1 = (F4(),F5()) <>0_goto 2;
set i2 = goto ((card F3()) + 2);
set i3 = goto (- ((card F3()) + 2));
set b = DataLoc ((F2() . F4()),F5());
A14:
IC ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))) = 0
by SCMPDS_6:21;
set mI = LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())));
set s5 = Comput ((ProgramPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1))),(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1)),(LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))));
set l2 = (card F3()) + 2;
A15:
while<>0 (F4(),F5(),F3()) = ((F4(),F5()) <>0_goto 2) ';' (((goto ((card F3()) + 2)) ';' F3()) ';' (goto (- ((card F3()) + 2))))
by Lm10;
set m3 = (LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1;
set s6 = Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1));
(card F3()) + 2 < (card F3()) + 3
by XREAL_1:8;
then A16:
(card F3()) + 2 in dom (while<>0 (F4(),F5(),F3()))
by Th13;
set s7 = Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),(((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1) + 1));
A17:
IExec (F3(),F2()) = (Result ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) +* (F2() | NAT)
by SCMPDS_4:def 8;
A18:
dom (ProgramPart F2()) = NAT
by COMPOS_1:34;
( while<>0 (F4(),F5(),F3()) c= Initialize (stop (while<>0 (F4(),F5(),F3()))) & Initialize (stop (while<>0 (F4(),F5(),F3()))) c= (Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))) )
by A6, FUNCT_4:26, SCMPDS_6:17;
then A19:
while<>0 (F4(),F5(),F3()) c= (Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))
by XBOOLE_1:1;
deffunc H1( State of SCMPDS) -> Element of NAT = F1($1);
A20:
for t being State of SCMPDS st P1[ Dstate t] & H1( Dstate t) = 0 holds
t . (DataLoc ((F2() . F4()),F5())) = 0
by A3;
A21:
for t being State of SCMPDS st P1[ Dstate t] & t . F4() = F2() . F4() & t . (DataLoc ((F2() . F4()),F5())) <> 0 holds
( (IExec (F3(),t)) . F4() = t . F4() & F3() is_closed_on t & F3() is_halting_on t & H1( Dstate (IExec (F3(),t))) < H1( Dstate t) & P1[ Dstate (IExec (F3(),t))] )
by A5;
A22: Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),(0 + 1)) =
Following ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),0)))
by EXTPRO_1:4
.=
Following ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))))
by EXTPRO_1:3
.=
Exec (((F4(),F5()) <>0_goto 2),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))))
by A15, A6, SCMPDS_6:22
;
Shift (F3(),2) c= while<>0 (F4(),F5(),F3())
by Lm11;
then
Shift (F3(),2) c= (Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))
by A19, XBOOLE_1:1;
then A23:
Shift (F3(),2) c= Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1)
by AMI_1:81;
A24:
DataPart ((Initialize F2()) +* (stop F3())) = DataPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))
by COMPOS_1:138, FUNCT_7:134;
now let a be
Int_position ;
((Initialize F2()) +* (stop F3())) . a = (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1)) . athus ((Initialize F2()) +* (stop F3())) . a =
((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))) . a
by A24, SCMPDS_4:23
.=
(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1)) . a
by A22, SCMPDS_2:67
;
verum end;
then A25:
DataPart ((Initialize F2()) +* (stop F3())) = DataPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1))
by SCMPDS_4:23;
((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))) . (DataLoc ((((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))) . F4()),F5())) =
((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))) . (DataLoc ((F2() . F4()),F5()))
by SCMPDS_5:19
.=
F2() . (DataLoc ((F2() . F4()),F5()))
by SCMPDS_5:19
;
then A26: IC (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1)) =
ICplusConst (((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),2)
by A2, A22, SCMPDS_2:67
.=
0 + 2
by A14, SCMPDS_6:23
;
then A27:
IC (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1))),(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1)),(LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))))) = (card F3()) + 2
by A1, A9, A13, A10, A25, A23, SCMPDS_7:36;
A28:
(ProgramPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1)))) /. (IC (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1)))) = (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1))) . (IC (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1))))
by COMPOS_1:38;
ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))) = ProgramPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1))
by AMI_1:123;
then A29:
Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1)) = Comput ((ProgramPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1))),(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1)),(LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))))
by EXTPRO_1:5;
then A30: CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1)))),(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1)))) =
(Comput ((ProgramPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1))),(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1)),(LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))))) . ((card F3()) + 2)
by A1, A9, A13, A10, A26, A25, A23, A28, SCMPDS_7:36
.=
(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1)) . ((card F3()) + 2)
by AMI_1:54
.=
((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))) . ((card F3()) + 2)
by AMI_1:54
.=
(while<>0 (F4(),F5(),F3())) . ((card F3()) + 2)
by A16, A19, GRFUNC_1:8
.=
goto (- ((card F3()) + 2))
by Th15
;
A31:
ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))) = ProgramPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1)))
by AMI_1:123;
A32: Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),(((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1) + 1)) =
Following ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1))))
by EXTPRO_1:4
.=
Exec ((goto (- ((card F3()) + 2))),(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1))))
by A30, A31
;
then IC (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),(((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1) + 1))) =
ICplusConst ((Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1))),(0 - ((card F3()) + 2)))
by SCMPDS_2:66
.=
0
by A27, A29, SCMPDS_7:1
;
then A33:
IC ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))) = IC (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 2)))
by SCMPDS_6:21;
A34:
DataPart (Comput ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())),(LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))))) = DataPart (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1))),(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1)),(LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3()))))))
by A1, A9, A13, A10, A26, A25, A23, SCMPDS_7:36;
now let x be
Int_position ;
(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),(((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1) + 1))) . x = ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))) . xA35:
not
x in dom (Initialize (stop (while<>0 (F4(),F5(),F3()))))
by SCMPDS_4:31;
A36:
not
x in dom (F2() | NAT)
by A18, SCMPDS_2:53;
(Comput ((ProgramPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1))),(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),1)),(LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))))) . x =
(Comput ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())),(LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))))) . x
by A34, SCMPDS_4:23
.=
(Result ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) . x
by A11, EXTPRO_1:23
.=
(IExec (F3(),F2())) . x
by A17, A36, FUNCT_4:12
;
hence (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),(((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1) + 1))) . x =
(IExec (F3(),F2())) . x
by A29, A32, SCMPDS_2:66
.=
((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))) . x
by A35, A8, FUNCT_4:12
;
verum end;
then A37:
DataPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),(((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 1) + 1))) = DataPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))
by SCMPDS_4:23;
set m0 = LifeSpan ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))));
A38: dom (ProgramPart F2()) =
(dom F2()) /\ NAT
by RELAT_1:90
.=
(({(IC )} \/ SCM-Data-Loc) \/ NAT) /\ NAT
by SCMPDS_4:19
.=
NAT
by XBOOLE_1:21
;
A39: (IExec (F3(),F2())) | NAT =
((Result ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) +* (ProgramPart F2())) | NAT
by SCMPDS_4:def 8
.=
ProgramPart F2()
by A38, FUNCT_4:24
;
A40:
P1[ Dstate F2()]
by A4;
( while<>0 (F4(),F5(),F3()) is_closed_on F2() & while<>0 (F4(),F5(),F3()) is_halting_on F2() )
from SCPINVAR:sch 3(A1, A20, A40, A21);
then A41:
ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))) halts_on (Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))
by SCMPDS_6:def 3;
deffunc H2( State of SCMPDS) -> Element of NAT = H1($1);
set Es = IExec (F3(),F2());
set bj = DataLoc (((IExec (F3(),F2())) . F4()),F5());
A42:
(IExec (F3(),F2())) . F4() = F2() . F4()
by A2, A4, A5;
then A43:
for t being State of SCMPDS st P1[ Dstate t] & H2( Dstate t) = 0 holds
t . (DataLoc (((IExec (F3(),F2())) . F4()),F5())) = 0
by A3;
A44:
for t being State of SCMPDS st P1[ Dstate t] & t . F4() = (IExec (F3(),F2())) . F4() & t . (DataLoc (((IExec (F3(),F2())) . F4()),F5())) <> 0 holds
( (IExec (F3(),t)) . F4() = t . F4() & F3() is_closed_on t & F3() is_halting_on t & H2( Dstate (IExec (F3(),t))) < H2( Dstate t) & P1[ Dstate (IExec (F3(),t))] )
by A5, A42;
A45:
P1[ Dstate (IExec (F3(),F2()))]
by A2, A4, A5;
( while<>0 (F4(),F5(),F3()) is_closed_on IExec (F3(),F2()) & while<>0 (F4(),F5(),F3()) is_halting_on IExec (F3(),F2()) )
from SCPINVAR:sch 3(A1, A43, A45, A44);
then A46:
ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))) halts_on (Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))
by SCMPDS_6:def 3;
A47:
ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))) = ProgramPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 2)))
by AMI_1:123;
ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))) =
ProgramPart (((Result ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) +* (ProgramPart F2())) +* (Initialize (stop (while<>0 (F4(),F5(),F3())))))
by A8, SCMPDS_4:def 8
.=
(ProgramPart ((Result ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) +* (ProgramPart F2()))) +* (ProgramPart (Initialize (stop (while<>0 (F4(),F5(),F3())))))
by FUNCT_4:75
.=
(ProgramPart F2()) +* (ProgramPart (Initialize (stop (while<>0 (F4(),F5(),F3())))))
by A38, FUNCT_4:24
.=
ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))
by A6, FUNCT_4:75
.=
ProgramPart (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 2)))
by AMI_1:123
;
then A48:
Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 2)) = (Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))
by A37, A33, SCMPDS_7:7;
then
CurInstr ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 2)))) = (F4(),F5()) <>0_goto 2
by A15, A47, A8, SCMPDS_6:22;
then
LifeSpan ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))) > (LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 2
by A41, SCMPDS_6:2, SCMPDS_6:29;
then consider nn being Nat such that
A49:
LifeSpan ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))) = ((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 2) + nn
by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 13;
A50:
ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))) = ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))
by A48, AMI_1:123;
then
Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),(((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 2) + (LifeSpan ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))))))) = Comput ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))),(LifeSpan ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))))))
by A48, EXTPRO_1:5;
then
CurInstr ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),(Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),(((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 2) + (LifeSpan ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))))))))) = halt SCMPDS
by A46, A50, EXTPRO_1:def 14;
then
((LifeSpan ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) + 2) + (LifeSpan ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))))) >= LifeSpan ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))))
by A41, EXTPRO_1:def 14;
then A51:
LifeSpan ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))) >= nn
by A49, XREAL_1:8;
A52:
Comput ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3())))),(LifeSpan ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))))) = Comput ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))),nn)
by A48, A49, A50, EXTPRO_1:5;
then
CurInstr ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),(Comput ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))),nn))) = halt SCMPDS
by A41, A50, EXTPRO_1:def 14;
then
nn >= LifeSpan ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))))
by A46, EXTPRO_1:def 14;
then
nn = LifeSpan ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))))
by A51, XXREAL_0:1;
then
Result ((ProgramPart ((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<>0 (F4(),F5(),F3()))))) = Comput ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))),(LifeSpan ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))))))
by A41, A52, EXTPRO_1:23;
hence IExec ((while<>0 (F4(),F5(),F3())),F2()) =
(Comput ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))),(LifeSpan ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))))))) +* (ProgramPart F2())
by SCMPDS_4:def 8
.=
(Result ((ProgramPart ((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<>0 (F4(),F5(),F3())))))) +* ((IExec (F3(),F2())) | NAT)
by A46, A39, EXTPRO_1:23
.=
IExec ((while<>0 (F4(),F5(),F3())),(IExec (F3(),F2())))
by SCMPDS_4:def 8
;
verum