set b = DataLoc (F1() . F3()),F4();
set i1 = F3(),F4() <=0_goto ((card F2()) + 3);
set J = F2() ';' (AddTo F3(),F4(),(- F5()));
set i3 = goto (- ((card F2()) + 2));
set FOR = for-down F3(),F4(),F5(),F2();
set iFOR = Initialized (stop (for-down F3(),F4(),F5(),F2()));
set iJ = Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))));
set s1 = F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())));
set ps = F1() | NAT ;
A5: P1[ Dstate F1()] by A3;
A6: for t being State of SCMPDS st P1[ Dstate t] & t . F3() = F1() . F3() & t . (DataLoc (F1() . F3()),F4()) > 0 holds
( (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . F3() = t . F3() & (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . (DataLoc (F1() . F3()),F4()) = (t . (DataLoc (F1() . F3()),F4())) - F5() & F2() is_closed_on t & F2() is_halting_on t & P1[ Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t)] ) by A4;
( ( P1[F1()] or not P1[F1()] ) & for-down F3(),F4(),F5(),F2() is_closed_on F1() & for-down F3(),F4(),F5(),F2() is_halting_on F1() ) from SCPISORT:sch 1(A1, A5, A6);
 then A7: F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))) is halting by SCMPDS_6:def 3;
set sJ = F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))));
set mJ = LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))));
set m1 = (LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2;
set s2 = (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())));
set m2 = LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))));
set Es = IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1();
set bj = DataLoc ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . F3()),F4();
A8: card (F2() ';' (AddTo F3(),F4(),(- F5()))) = (card F2()) + 1 by SCMP_GCD:8;
A9: ( (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . F3() = F1() . F3() & (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . (DataLoc (F1() . F3()),F4()) = (F1() . (DataLoc (F1() . F3()),F4())) - F5() & F2() is_closed_on F1() & F2() is_halting_on F1() & P1[ Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())] ) by A2, A3, A4;
then A10: ( F2() ';' (AddTo F3(),F4(),(- F5())) is_closed_on F1() & F2() ';' (AddTo F3(),F4(),(- F5())) is_halting_on F1() ) by Th6;
A11: P1[ Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())] by A2, A3, A4;
A12: for t being State of SCMPDS st P1[ Dstate t] & t . F3() = (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . F3() & t . (DataLoc ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . F3()),F4()) > 0 holds
( (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . F3() = t . F3() & (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . (DataLoc ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . F3()),F4()) = (t . (DataLoc ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . F3()),F4())) - F5() & F2() is_closed_on t & F2() is_halting_on t & P1[ Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t)] ) by A4, A9;
A13: ( ( P1[ IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()] or not P1[ IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()] ) & for-down F3(),F4(),F5(),F2() is_closed_on IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1() & for-down F3(),F4(),F5(),F2() is_halting_on IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1() ) from SCPISORT:sch 1(A1, A11, A12);
 set s4 = Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1;
A14: Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))) c= F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))) by FUNCT_4:26;
A15: F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))) is halting by A10, SCMPDS_6:def 3;
then (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))) is halting by A14, FUNCT_4:79;
then A16: F2() ';' (AddTo F3(),F4(),(- F5())) is_halting_on F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))) by SCMPDS_6:def 3;
A17: F2() ';' (AddTo F3(),F4(),(- F5())) is_closed_on F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))) by A10, SCMPDS_6:38;
A18: IC (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) = inspos 0 by SCMPDS_6:21;
A19: for-down F3(),F4(),F5(),F2() = (F3(),F4() <=0_goto ((card F2()) + 3)) ';' ((F2() ';' (AddTo F3(),F4(),(- F5()))) ';' (goto (- ((card F2()) + 2)))) by Lm3;
then A20: CurInstr (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) = F3(),F4() <=0_goto ((card F2()) + 3) by SCMPDS_6:22;
A21: Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(0 + 1) = Following (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),0 ) by AMI_1:14
.= Following (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) by AMI_1:13
.= Exec (F3(),F4() <=0_goto ((card F2()) + 3)),(F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) by A20, AMI_1:def 18 ;
A22: ( not F3() in dom (Initialized (stop (for-down F3(),F4(),F5(),F2()))) & F3() in dom F1() ) by SCMPDS_2:49, SCMPDS_4:31;
A23: ( not DataLoc (F1() . F3()),F4() in dom (Initialized (stop (for-down F3(),F4(),F5(),F2()))) & DataLoc (F1() . F3()),F4() in dom F1() ) by SCMPDS_2:49, SCMPDS_4:31;
A24: (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . (DataLoc ((F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . F3()),F4()) = (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . (DataLoc (F1() . F3()),F4()) by A22, FUNCT_4:12
.= F1() . (DataLoc (F1() . F3()),F4()) by A23, FUNCT_4:12 ;
A25: IC (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1) = (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1) . (IC SCMPDS ) by AMI_1:def 15
.= Next (IC (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))) by A2, A21, A24, SCMPDS_2:68
.= inspos (0 + 1) by A18 ;
A26: DataPart (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) = DataPart (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) by SCMPDS_4:24, SCMPDS_4:36;
now
let x be Int_position ; :: thesis: (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) . x = (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1) . x
thus (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) . x = (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . x by A26, SCMPDS_4:23
.= (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1) . x by A21, SCMPDS_2:68 ; :: thesis: verum
end;
then A27: DataPart (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))) = DataPart (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1) by SCMPDS_4:23;
set s5 = Computation (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1),(LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))));
set l1 = inspos ((card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1);
A28: IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1() = (Result (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) +* (F1() | NAT ) by SCMPDS_4:def 8;
A29: dom (F1() | NAT ) = NAT by SCMPDS_6:1;
(card F2()) + 2 < (card F2()) + 3 by XREAL_1:8;
then A30: inspos ((card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1) in dom (for-down F3(),F4(),F5(),F2()) by A8, SCMPDS_7:61;
A31: for-down F3(),F4(),F5(),F2() c= Initialized (stop (for-down F3(),F4(),F5(),F2())) by SCMPDS_6:17;
Initialized (stop (for-down F3(),F4(),F5(),F2())) c= F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))) by FUNCT_4:26;
then A32: for-down F3(),F4(),F5(),F2() c= F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))) by A31, XBOOLE_1:1;
Shift (F2() ';' (AddTo F3(),F4(),(- F5()))),1 c= for-down F3(),F4(),F5(),F2() by Lm4;
then Shift (F2() ';' (AddTo F3(),F4(),(- F5()))),1 c= F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))) by A32, XBOOLE_1:1;
then A33: Shift (F2() ';' (AddTo F3(),F4(),(- F5()))),1 c= Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1 by AMI_1:81;
then A34: DataPart (Computation (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),(LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))))) = DataPart (Computation (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1),(LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))))) by A8, A14, A16, A17, A25, A27, SCMPDS_7:36;
set m3 = (LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1;
set s6 = Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1);
A35: IC (Computation (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1),(LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))))) = inspos ((card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1) by A8, A14, A16, A17, A25, A27, A33, SCMPDS_7:36;
A36: Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) = Computation (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1),(LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) by AMI_1:51;
then A37: CurInstr (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1)) = (Computation (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1),(LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))))) . (inspos ((card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1)) by A35, AMI_1:def 17
.= (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1) . (inspos ((card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1)) by AMI_1:54
.= (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . (inspos ((card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1)) by AMI_1:54
.= (for-down F3(),F4(),F5(),F2()) . (inspos ((card (F2() ';' (AddTo F3(),F4(),(- F5())))) + 1)) by A30, A32, GRFUNC_1:8
.= goto (- ((card F2()) + 2)) by A8, SCMPDS_7:62 ;
set m4 = ((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1;
set s7 = Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1);
A38: Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1) = Following (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1)) by AMI_1:14
.= Exec (goto (- ((card F2()) + 2))),(Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1)) by A37, AMI_1:def 18 ;
A39: IC (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1)) = (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1)) . (IC SCMPDS ) by AMI_1:def 15
.= ICplusConst (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1)),(0 - ((card F2()) + 2)) by A38, SCMPDS_2:66
.= inspos 0 by A8, A35, A36, SCMPDS_7:1 ;
now
let x be Int_position ; :: thesis: (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1)) . x = ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . x
( not x in dom (Initialized (stop (for-down F3(),F4(),F5(),F2()))) & x in dom (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) ) by SCMPDS_2:49, SCMPDS_4:31;
then A40: ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . x = (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . x by FUNCT_4:12;
A41: now
assume x in dom (F1() | NAT ) ; :: thesis: contradiction
then reconsider l = x as Instruction-Location of SCMPDS by A29, AMI_1:def 4;
l = x ;
hence contradiction by SCMPDS_2:53; :: thesis: verum
end;
(Computation (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),1),(LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))))) . x = (Computation (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))),(LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5())))))))) . x by A34, SCMPDS_4:23
.= (Result (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) . x by A15, AMI_1:122
.= (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) . x by A28, A41, FUNCT_4:12 ;
hence (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1)) . x = ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) . x by A36, A38, A40, SCMPDS_2:66; :: thesis: verum
end;
then A42: DataPart (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 1) + 1)) = DataPart ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) by SCMPDS_4:23;
A43: IC ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) = IC (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2)) by A39, SCMPDS_6:21;
A44: (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))) is halting by A13, SCMPDS_6:def 3;
A45: dom (F1() | NAT ) = (dom F1()) /\ NAT by RELAT_1:90
.= (({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT ) /\ NAT by SCMPDS_4:19
.= NAT by XBOOLE_1:21 ;
((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) | NAT = (((Result (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) +* (F1() | NAT )) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) | NAT by SCMPDS_4:def 8
.= (((Result (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) +* (F1() | NAT )) | NAT ) +* ((Initialized (stop (for-down F3(),F4(),F5(),F2()))) | NAT ) by FUNCT_4:75
.= (F1() | NAT ) +* ((Initialized (stop (for-down F3(),F4(),F5(),F2()))) | NAT ) by A45, FUNCT_4:24
.= (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) | NAT by FUNCT_4:75
.= (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2)) | NAT by SCMPDS_7:6 ;
then A46: Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2) = (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))) by A42, A43, SCMPDS_7:7;
then A47: CurInstr (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2)) = F3(),F4() <=0_goto ((card F2()) + 3) by A19, SCMPDS_6:22;
set m0 = LifeSpan (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))));
LifeSpan (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) > (LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2 by A7, A47, SCMPDS_6:2, SCMPDS_6:30;
then consider nn being Nat such that
A48: LifeSpan (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) = ((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2) + nn by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 13;
A49: Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(LifeSpan (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))) = Computation ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),nn by A46, A48, AMI_1:51;
then CurInstr (Computation ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),nn) = halt SCMPDS by A7, AMI_1:def 46;
then A50: nn >= LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) by A44, AMI_1:def 46;
Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2) + (LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))))) = Computation ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))) by A46, AMI_1:51;
then CurInstr (Computation (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2) + (LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))))) = halt SCMPDS by A44, AMI_1:def 46;
then ((LifeSpan (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) + 2) + (LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))) >= LifeSpan (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) by A7, AMI_1:def 46;
then LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) >= nn by A48, XREAL_1:8;
then nn = LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) by A50, XXREAL_0:1;
then A51: Result (F1() +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))) = Computation ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))) by A7, A49, AMI_1:122;
A52: (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) | NAT = ((Result (F1() +* (Initialized (stop (F2() ';' (AddTo F3(),F4(),(- F5()))))))) +* (F1() | NAT )) | NAT by SCMPDS_4:def 8
.= F1() | NAT by A45, FUNCT_4:24 ;
thus ( P1[F1()] or not P1[F1()] ) ; :: thesis: IExec (for-down F3(),F4(),F5(),F2()),F1() = IExec (for-down F3(),F4(),F5(),F2()),(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1())
thus IExec (for-down F3(),F4(),F5(),F2()),F1() = (Computation ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))),(LifeSpan ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2())))))) +* (F1() | NAT ) by A51, SCMPDS_4:def 8
.= (Result ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) +* (Initialized (stop (for-down F3(),F4(),F5(),F2()))))) +* ((IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) | NAT ) by A44, A52, AMI_1:122
.= IExec (for-down F3(),F4(),F5(),F2()),(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) by SCMPDS_4:def 8 ; :: thesis: verum