set WHL = while<>0 F4(),F5(),F3();
set s1 = (Initialize F2()) +* (stop (while<>0 F4(),F5(),F3()));
set ps = ProgramPart F2();
I1:
(Initialize F2()) +* (stop (while<>0 F4(),F5(),F3())) = F2() +* (Initialize (stop (while<>0 F4(),F5(),F3())))
by SCMPDS_4:5;
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())));
I2:
(Initialize F2()) +* (stop F3()) = F2() +* (Initialize (stop F3()))
by SCMPDS_4:5;
I3:
(Initialize (IExec F3(),F2())) +* (stop (while<>0 F4(),F5(),F3())) = (IExec F3(),F2()) +* (Initialize (stop (while<>0 F4(),F5(),F3())))
by SCMPDS_4:5;
A6:
Initialize (stop F3()) c= (Initialize F2()) +* (stop F3())
by I2, FUNCT_4:26;
F3() is_closed_on F2()
by A2, A4, A5;
then A7:
F3() is_closed_on (Initialize F2()) +* (stop F3())
by SCMPDS_6:38;
F3() is_halting_on F2()
by A2, A4, A5;
then A8:
ProgramPart ((Initialize F2()) +* (stop F3())) halts_on (Initialize F2()) +* (stop F3())
by SCMPDS_6:def 3;
I4:
(Initialize ((Initialize F2()) +* (stop F3()))) +* (stop F3()) = ((Initialize F2()) +* (stop F3())) +* (Initialize (stop F3()))
by SCMPDS_4:5;
(Initialize F2()) +* (stop F3()) = (Initialize ((Initialize F2()) +* (stop F3()))) +* (stop F3())
by A6, I4, FUNCT_4:79;
then
ProgramPart ((Initialize ((Initialize F2()) +* (stop F3()))) +* (stop F3())) halts_on (Initialize ((Initialize F2()) +* (stop F3()))) +* (stop F3())
by A8;
then A9:
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();
A10:
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;
A11:
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 A12:
(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);
A13:
IExec F3(),F2() = (Result (ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3()))) +* (F2() | NAT )
by SCMPDS_4:def 8;
A14:
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 I1, FUNCT_4:26, SCMPDS_6:17;
then A15:
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);
A16:
for t being State of SCMPDS st P1[ Dstate t] & H1( Dstate t) = 0 holds
t . (DataLoc (F2() . F4()),F5()) = 0
by A3;
A17:
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;
A18: 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 AMI_1:14
.=
Following (ProgramPart ((Initialize F2()) +* (stop (while<>0 F4(),F5(),F3())))),((Initialize F2()) +* (stop (while<>0 F4(),F5(),F3())))
by AMI_1:13
.=
Exec (F4(),F5() <>0_goto 2),((Initialize F2()) +* (stop (while<>0 F4(),F5(),F3())))
by A11, I1, 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 A15, XBOOLE_1:1;
then A19:
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;
A20:
DataPart ((Initialize F2()) +* (stop F3())) = DataPart ((Initialize F2()) +* (stop (while<>0 F4(),F5(),F3())))
by FUNCT_7:134, SCMPDS_4:24;
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 A20, SCMPDS_4:23
.=
(Comput (ProgramPart ((Initialize F2()) +* (stop (while<>0 F4(),F5(),F3())))),((Initialize F2()) +* (stop (while<>0 F4(),F5(),F3()))),1) . a
by A18, SCMPDS_2:67
;
verum end;
then A21:
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 A22: 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, A18, SCMPDS_2:67
.=
0 + 2
by A10, SCMPDS_6:23
;
then A23:
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, A6, A9, A7, A21, A19, SCMPDS_7:36;
Y:
(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 A24:
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 AMI_1:51;
then A25: 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, A6, A9, A7, A22, A21, A19, Y, 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 A12, A15, GRFUNC_1:8
.=
goto (- ((card F3()) + 2))
by Th15
;
T:
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;
A26: 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 AMI_1:14
.=
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 A25, T
;
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 A23, A24, SCMPDS_7:1
;
then A27:
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;
A28:
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, A6, A9, A7, A22, A21, A19, 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()))) . xA29:
not
x in dom (Initialize (stop (while<>0 F4(),F5(),F3())))
by SCMPDS_4:31;
A30:
not
x in dom (F2() | NAT )
by A14, 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 A28, SCMPDS_4:23
.=
(Result (ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3()))) . x
by A8, AMI_1:122
.=
(IExec F3(),F2()) . x
by A13, A30, 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 A24, A26, SCMPDS_2:66
.=
((Initialize (IExec F3(),F2())) +* (stop (while<>0 F4(),F5(),F3()))) . x
by A29, I3, FUNCT_4:12
;
verum end;
then A31:
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())));
A32: dom (ProgramPart F2()) =
(dom F2()) /\ NAT
by RELAT_1:90
.=
(({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT ) /\ NAT
by SCMPDS_4:19
.=
NAT
by XBOOLE_1:21
;
A33: (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 A32, FUNCT_4:24
;
A34:
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, A16, A34, A17);
then A35:
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();
A36:
(IExec F3(),F2()) . F4() = F2() . F4()
by A2, A4, A5;
then A37:
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;
A38:
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, A36;
A39:
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, A37, A39, A38);
then A40:
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;
NX:
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 I3, 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 A32, FUNCT_4:24
.=
ProgramPart ((Initialize F2()) +* (stop (while<>0 F4(),F5(),F3())))
by I1, 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 A41:
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 A31, A27, 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 A11, NX, I3, 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 A35, SCMPDS_6:2, SCMPDS_6:29;
then consider nn being Nat such that
A42:
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;
T:
ProgramPart ((Initialize F2()) +* (stop (while<>0 F4(),F5(),F3()))) = ProgramPart ((Initialize (IExec F3(),F2())) +* (stop (while<>0 F4(),F5(),F3())))
by A41, 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 A41, AMI_1:51;
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 A40, T, AMI_1:def 46;
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 A35, AMI_1:def 46;
then A43:
LifeSpan (ProgramPart ((Initialize (IExec F3(),F2())) +* (stop (while<>0 F4(),F5(),F3())))),((Initialize (IExec F3(),F2())) +* (stop (while<>0 F4(),F5(),F3()))) >= nn
by A42, XREAL_1:8;
A44:
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 A41, A42, T, AMI_1:51;
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 A35, T, AMI_1:def 46;
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 A40, AMI_1:def 46;
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 A43, 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 A35, A44, AMI_1:122;
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 A40, A33, AMI_1:122
.=
IExec (while<>0 F4(),F5(),F3()),(IExec F3(),F2())
by SCMPDS_4:def 8
;
verum