set WHL = while<>0 F4(),F5(),F3();
set iWH = Initialized (stop (while<>0 F4(),F5(),F3()));
set iI = Initialized (stop F3());
set s1 = F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())));
set ps = F2() | NAT ;
set sI = F2() +* (Initialized (stop F3()));
set m1 = (LifeSpan (F2() +* (Initialized (stop F3())))) + 2;
set s2 = (IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())));
set m2 = LifeSpan ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3()))));
A6: Initialized (stop F3()) c= F2() +* (Initialized (stop F3())) by FUNCT_4:26;
F3() is_closed_on F2() by A2, A4, A5;
then A7: F3() is_closed_on F2() +* (Initialized (stop F3())) by SCMPDS_6:38;
F3() is_halting_on F2() by A2, A4, A5;
then A8: ProgramPart (F2() +* (Initialized (stop F3()))) halts_on F2() +* (Initialized (stop F3())) by SCMPDS_6:def 3;
F2() +* (Initialized (stop F3())) = (F2() +* (Initialized (stop F3()))) +* (Initialized (stop F3())) by A6, FUNCT_4:79;
then ProgramPart ((F2() +* (Initialized (stop F3()))) +* (Initialized (stop F3()))) halts_on (F2() +* (Initialized (stop F3()))) +* (Initialized (stop F3())) by A8;
then A9: F3() is_halting_on F2() +* (Initialized (stop F3())) by SCMPDS_6:def 3;
set s4 = Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (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 (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) = 0 by SCMPDS_6:21;
set mI = LifeSpan (F2() +* (Initialized (stop F3())));
set s5 = Comput (ProgramPart (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1)),(Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1),(LifeSpan (F2() +* (Initialized (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 (F2() +* (Initialized (stop F3())))) + 1;
set s6 = Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (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 (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(((LifeSpan (F2() +* (Initialized (stop F3())))) + 1) + 1);
A13: IExec F3(),F2() = (Result (F2() +* (Initialized (stop F3())))) +* (F2() | NAT ) by SCMPDS_4:def 8;
A14: dom (F2() | NAT ) = NAT by SCMPDS_6:1;
( while<>0 F4(),F5(),F3() c= Initialized (stop (while<>0 F4(),F5(),F3())) & Initialized (stop (while<>0 F4(),F5(),F3())) c= F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))) ) by FUNCT_4:26, SCMPDS_6:17;
then A15: while<>0 F4(),F5(),F3() c= F2() +* (Initialized (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 (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(0 + 1) = Following (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),0 ) by AMI_1:14
.= Following (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) by AMI_1:13
.= Exec (F4(),F5() <>0_goto 2),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) by A11, SCMPDS_6:22 ;
Shift F3(),2 c= while<>0 F4(),F5(),F3() by Lm11;
then Shift F3(),2 c= F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))) by A15, XBOOLE_1:1;
then A19: Shift F3(),2 c= Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1 by AMI_1:81;
A20: DataPart (F2() +* (Initialized (stop F3()))) = DataPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) by SCMPDS_4:24, SCMPDS_4:36;
now
let a be Int_position ; :: thesis: (F2() +* (Initialized (stop F3()))) . a = (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1) . a
thus (F2() +* (Initialized (stop F3()))) . a = (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) . a by A20, SCMPDS_4:23
.= (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1) . a by A18, SCMPDS_2:67 ; :: thesis: verum
end;
then A21: DataPart (F2() +* (Initialized (stop F3()))) = DataPart (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1) by SCMPDS_4:23;
(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) . (DataLoc ((F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) . F4()),F5()) = (F2() +* (Initialized (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 (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1) = ICplusConst (F2() +* (Initialized (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 (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1)),(Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1),(LifeSpan (F2() +* (Initialized (stop F3()))))) = (card F3()) + 2 by A1, A6, A9, A7, A21, A19, SCMPDS_7:36;
Y: (ProgramPart (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 1))) /. (IC (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 1))) = (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 1)) . (IC (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 1))) by AMI_1:150;
ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) = ProgramPart (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1) by AMI_1:144;
then A24: Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 1) = Comput (ProgramPart (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1)),(Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1),(LifeSpan (F2() +* (Initialized (stop F3())))) by AMI_1:51;
then A25: CurInstr (ProgramPart (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 1))),(Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 1)) = (Comput (ProgramPart (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1)),(Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1),(LifeSpan (F2() +* (Initialized (stop F3()))))) . ((card F3()) + 2) by A1, A6, A9, A7, A22, A21, A19, SCMPDS_7:36, Y
.= (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1) . ((card F3()) + 2) by AMI_1:54
.= (F2() +* (Initialized (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 (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) = ProgramPart (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 1)) by AMI_1:144;
A26: Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(((LifeSpan (F2() +* (Initialized (stop F3())))) + 1) + 1) = Following (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 1)) by AMI_1:14
.= Exec (goto (- ((card F3()) + 2))),(Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 1)) by A25, T ;
then IC (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(((LifeSpan (F2() +* (Initialized (stop F3())))) + 1) + 1)) = ICplusConst (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 1)),(0 - ((card F3()) + 2)) by SCMPDS_2:66
.= 0 by A23, A24, SCMPDS_7:1 ;
then A27: IC ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))) = IC (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 2)) by SCMPDS_6:21;
A28: DataPart (Comput (ProgramPart (F2() +* (Initialized (stop F3())))),(F2() +* (Initialized (stop F3()))),(LifeSpan (F2() +* (Initialized (stop F3()))))) = DataPart (Comput (ProgramPart (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1)),(Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1),(LifeSpan (F2() +* (Initialized (stop F3()))))) by A1, A6, A9, A7, A22, A21, A19, SCMPDS_7:36;
now
let x be Int_position ; :: thesis: (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(((LifeSpan (F2() +* (Initialized (stop F3())))) + 1) + 1)) . x = ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))) . x
A29: not x in dom (Initialized (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 (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1)),(Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),1),(LifeSpan (F2() +* (Initialized (stop F3()))))) . x = (Comput (ProgramPart (F2() +* (Initialized (stop F3())))),(F2() +* (Initialized (stop F3()))),(LifeSpan (F2() +* (Initialized (stop F3()))))) . x by A28, SCMPDS_4:23
.= (Result (F2() +* (Initialized (stop F3())))) . x by A8, AMI_1:122
.= (IExec F3(),F2()) . x by A13, A30, FUNCT_4:12 ;
hence (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(((LifeSpan (F2() +* (Initialized (stop F3())))) + 1) + 1)) . x = (IExec F3(),F2()) . x by A24, A26, SCMPDS_2:66
.= ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))) . x by A29, FUNCT_4:12 ;
:: thesis: verum
end;
then A31: DataPart (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(((LifeSpan (F2() +* (Initialized (stop F3())))) + 1) + 1)) = DataPart ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))) by SCMPDS_4:23;
set m0 = LifeSpan (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))));
A32: dom (F2() | NAT ) = (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 (F2() +* (Initialized (stop F3())))) +* (F2() | NAT )) | NAT by SCMPDS_4:def 8
.= F2() | NAT 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 (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) halts_on F2() +* (Initialized (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 ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))) halts_on (IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3()))) by SCMPDS_6:def 3;
((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))) | NAT = (((Result (F2() +* (Initialized (stop F3())))) +* (F2() | NAT )) +* (Initialized (stop (while<>0 F4(),F5(),F3())))) | NAT by SCMPDS_4:def 8
.= (((Result (F2() +* (Initialized (stop F3())))) +* (F2() | NAT )) | NAT ) +* ((Initialized (stop (while<>0 F4(),F5(),F3()))) | NAT ) by FUNCT_4:75
.= (F2() | NAT ) +* ((Initialized (stop (while<>0 F4(),F5(),F3()))) | NAT ) by A32, FUNCT_4:24
.= (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) | NAT by FUNCT_4:75
.= (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 2)) | NAT by SCMPDS_7:6 ;
then A41: Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 2) = (IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3()))) by A31, A27, SCMPDS_7:7;
then CurInstr (ProgramPart (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 2))),(Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),((LifeSpan (F2() +* (Initialized (stop F3())))) + 2)) = F4(),F5() <>0_goto 2 by A11, SCMPDS_6:22;
then LifeSpan (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) > (LifeSpan (F2() +* (Initialized (stop F3())))) + 2 by A35, SCMPDS_6:2, SCMPDS_6:29;
then consider nn being Nat such that
A42: LifeSpan (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) = ((LifeSpan (F2() +* (Initialized (stop F3())))) + 2) + nn by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 13;
T: ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) = ProgramPart ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))) by A41, AMI_1:144;
then Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(((LifeSpan (F2() +* (Initialized (stop F3())))) + 2) + (LifeSpan ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))))) = Comput (ProgramPart ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(LifeSpan ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3()))))) by A41, AMI_1:51;
then CurInstr (ProgramPart (Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(((LifeSpan (F2() +* (Initialized (stop F3())))) + 2) + (LifeSpan ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))))))),(Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(((LifeSpan (F2() +* (Initialized (stop F3())))) + 2) + (LifeSpan ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3()))))))) = halt SCMPDS by A40, AMI_1:def 46;
then ((LifeSpan (F2() +* (Initialized (stop F3())))) + 2) + (LifeSpan ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3()))))) >= LifeSpan (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) by A35, AMI_1:def 46;
then A43: LifeSpan ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))) >= nn by A42, XREAL_1:8;
A44: Comput (ProgramPart (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),(F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(LifeSpan (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3()))))) = Comput (ProgramPart ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))),nn by A41, A42, AMI_1:51, T;
then CurInstr (ProgramPart (Comput (ProgramPart ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))),nn)),(Comput (ProgramPart ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))),nn) = halt SCMPDS by A35, AMI_1:def 46;
then nn >= LifeSpan ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))) by A40, AMI_1:def 46;
then nn = LifeSpan ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))) by A43, XXREAL_0:1;
then Result (F2() +* (Initialized (stop (while<>0 F4(),F5(),F3())))) = Comput (ProgramPart ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(LifeSpan ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3()))))) by A35, A44, AMI_1:122;
hence IExec (while<>0 F4(),F5(),F3()),F2() = (Comput (ProgramPart ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3()))))),((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))),(LifeSpan ((IExec F3(),F2()) +* (Initialized (stop (while<>0 F4(),F5(),F3())))))) +* (F2() | NAT ) by SCMPDS_4:def 8
.= (Result ((IExec F3(),F2()) +* (Initialized (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 ;
:: thesis: verum