set WHL = while<0 (F4(),F5(),F3());
set pWHL = stop (while<0 (F4(),F5(),F3()));
set s1 = (Initialize F2()) +* (stop (while<0 (F4(),F5(),F3())));
set ps = ProgramPart F2();
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())))));
A6: (Initialize F2()) +* (stop (while<0 (F4(),F5(),F3()))) = F2() +* (Initialize (stop (while<0 (F4(),F5(),F3())))) by COMPOS_1:125;
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: P1[ Dstate F2()] by A4;
A10: Initialize (stop F3()) c= (Initialize F2()) +* (stop F3()) by A7, FUNCT_4:26;
F3() is_closed_on F2() by A2, A4, A5;
then A11: F3() is_closed_on (Initialize F2()) +* (stop F3()) by SCMPDS_6:38;
F3() is_halting_on F2() by A2, A4, A5;
then A12: ProgramPart ((Initialize F2()) +* (stop F3())) halts_on (Initialize F2()) +* (stop F3()) by SCMPDS_6:def 3;
A13: (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 A10, A13, FUNCT_4:79;
then ProgramPart ((Initialize ((Initialize F2()) +* (stop F3()))) +* (stop F3())) halts_on (Initialize ((Initialize F2()) +* (stop F3()))) +* (stop F3()) by A12;
then A14: F3() is_halting_on (Initialize F2()) +* (stop F3()) by SCMPDS_6:def 3;
set Es = IExec (F3(),F2());
set bj = DataLoc (((IExec (F3(),F2())) . F4()),F5());
deffunc H1( State of SCMPDS) -> Element of NAT = F1($1);
A15: 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;
A16: for t being State of SCMPDS st P1[ Dstate t] & H1( Dstate t) = 0 holds
t . (DataLoc ((F2() . F4()),F5())) >= 0 by A3;
( ( H1(F2()) = H1(F2()) or P1[F2()] ) & while<0 (F4(),F5(),F3()) is_closed_on F2() & while<0 (F4(),F5(),F3()) is_halting_on F2() ) from SCMPDS_8:sch 1(A1, A16, A9, A15);
 then A17: 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 = F1($1);
A18: (IExec (F3(),F2())) . F4() = F2() . F4() by A2, A4, A5;
then A19: 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;
A20: 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, A18;
A21: P1[ Dstate (IExec (F3(),F2()))] by A2, A4, A5;
( ( H2( IExec (F3(),F2())) = H2( IExec (F3(),F2())) or P1[ IExec (F3(),F2())] ) & while<0 (F4(),F5(),F3()) is_closed_on IExec (F3(),F2()) & while<0 (F4(),F5(),F3()) is_halting_on IExec (F3(),F2()) ) from SCMPDS_8:sch 1(A1, A19, A21, A20);
 then A22: 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;
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 ((card F3()) + 2);
set i2 = goto (- ((card F3()) + 1));
set b = DataLoc ((F2() . F4()),F5());
A23: while<0 (F4(),F5(),F3()) = ((F4(),F5()) >=0_goto ((card F3()) + 2)) ';' (F3() ';' (goto (- ((card F3()) + 1)))) by SCMPDS_4:51;
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 l1 = (card F3()) + 1;
A24: IC ((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3())))) = 0 by SCMPDS_6:21;
A25: 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 ((card F3()) + 2)),((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3()))))) by A23, A6, SCMPDS_6:22 ;
A26: 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 ; :: thesis: ((Initialize F2()) +* (stop F3())) . a = (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3())))),1)) . a
thus ((Initialize F2()) +* (stop F3())) . a = ((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3())))) . a by A26, SCMPDS_4:23
.= (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3())))),1)) . a by A25, SCMPDS_2:69 ; :: thesis: verum
end;
then A27: 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;
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()) + 1 < (card F3()) + 2 by XREAL_1:8;
then A28: (card F3()) + 1 in dom (while<0 (F4(),F5(),F3())) by Th7;
thus ( F1(F2()) = F1(F2()) or P1[F2()] ) ; :: thesis: IExec ((while<0 (F4(),F5(),F3())),F2()) = IExec ((while<0 (F4(),F5(),F3())),(IExec (F3(),F2())))
set m0 = LifeSpan ((ProgramPart ((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3())))));
A29: 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 ;
A30: (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 A29, FUNCT_4:24 ;
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));
A31: IExec (F3(),F2()) = (Result ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) +* (F2() | NAT) by SCMPDS_4:def 8;
A32: 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 A33: while<0 (F4(),F5(),F3()) c= (Initialize F2()) +* (stop (while<0 (F4(),F5(),F3()))) by XBOOLE_1:1;
Shift (F3(),1) c= while<0 (F4(),F5(),F3()) by Lm2;
then Shift (F3(),1) c= (Initialize F2()) +* (stop (while<0 (F4(),F5(),F3()))) by A33, XBOOLE_1:1;
then A34: Shift (F3(),1) c= Comput ((ProgramPart ((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3())))),1) by AMI_1:81;
((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 A35: IC (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3())))),1)) = succ (IC ((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3()))))) by A2, A25, SCMPDS_2:69
.= 0 + 1 by A24 ;
then A36: 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()) + 1 by A1, A10, A14, A11, A27, A34, SCMPDS_7:36;
A37: (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 A38: 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 A39: 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()) + 1) by A1, A10, A14, A11, A35, A27, A34, A37, SCMPDS_7:36
.= (Comput ((ProgramPart ((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3()))))),((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3())))),1)) . ((card F3()) + 1) by AMI_1:54
.= ((Initialize F2()) +* (stop (while<0 (F4(),F5(),F3())))) . ((card F3()) + 1) by AMI_1:54
.= (while<0 (F4(),F5(),F3())) . ((card F3()) + 1) by A28, A33, GRFUNC_1:8
.= goto (- ((card F3()) + 1)) by Th8 ;
A40: 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;
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())))) + 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()) + 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)))) by A39, A40 ;
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()) + 1))) by SCMPDS_2:66
.= 0 by A36, A38, SCMPDS_7:1 ;
then A42: 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;
A43: 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, A10, A14, A11, A35, A27, A34, SCMPDS_7:36;
now
let x be Int_position ; :: thesis: (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())))) . x
A44: not x in dom (Initialize (stop (while<0 (F4(),F5(),F3())))) by SCMPDS_4:31;
A45: not x in dom (F2() | NAT) by A32, 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 A43, SCMPDS_4:23
.= (Result ((ProgramPart ((Initialize F2()) +* (stop F3()))),((Initialize F2()) +* (stop F3())))) . x by A12, EXTPRO_1:23
.= (IExec (F3(),F2())) . x by A31, A45, 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 A38, A41, SCMPDS_2:66
.= ((Initialize (IExec (F3(),F2()))) +* (stop (while<0 (F4(),F5(),F3())))) . x by A44, A8, FUNCT_4:12 ;
:: thesis: verum
end;
then A46: 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;
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 A29, 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 A46, A42, 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 ((card F3()) + 2) by A23, 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 A17, SCMPDS_6:2, SCMPDS_6:31;
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;
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 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 A22, 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 A17, 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 F2()) +* (stop (while<0 (F4(),F5(),F3()))))),((Initialize (IExec (F3(),F2()))) +* (stop (while<0 (F4(),F5(),F3())))),nn) by A48, A49, 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 A17, 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 A22, 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 A17, A52, A50, 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 A22, A30, EXTPRO_1:23
.= IExec ((while<0 (F4(),F5(),F3())),(IExec (F3(),F2()))) by SCMPDS_4:def 8 ;
:: thesis: verum