set i1 = (F₄(),F₅()) <=0_goto ((card F₃()) + 3);
set J = F₃() ';' (AddTo (F₄(),F₅(),(- F₆())));
set i3 = goto (- ((card F₃()) + 2));
set FOR = for-down (F₄(),F₅(),F₆(),F₃());
set pFOR = stop (for-down (F₄(),F₅(),F₆(),F₃()));
set P1 = F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())));
set PJ = F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))));
set mJ = LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁());
set m1 = (LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 2;
set s2 = Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()));
set m2 = LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))));
A5: stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))) c= F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))))) by FUNCT_4:25;
A6: Initialize F₁() = F₁() by MEMSTR_0:44;
A7: ( F₃() is_closed_on F₁(),F₂() & F₃() is_halting_on F₁(),F₂() ) by A2, A3, A4;
then F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))) is_closed_on F₁(),F₂() by Th5;
then A8: F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))) is_closed_on F₁(),F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))))) by A6, SCMPDS_6:24;
A9: F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))) is_halting_on F₁(),F₂() by A7, Th5;
then A10: F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))))) halts_on F₁() by A6, SCMPDS_6:def 3;
(F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))) +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))))) halts_on Initialize F₁() by A9, SCMPDS_6:def 3;
then A11: F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))) is_halting_on F₁(),F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))))) by SCMPDS_6:def 3;
A12: for-down (F₄(),F₅(),F₆(),F₃()) = ((F₄(),F₅()) <=0_goto ((card F₃()) + 3)) ';' ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))) ';' (goto (- ((card F₃()) + 2)))) by Lm2;
A13: Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),(0 + 1)) = Following ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),0))) by EXTPRO_1:3
.= Following ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁()) by EXTPRO_1:2
.= Exec (((F₄(),F₅()) <=0_goto ((card F₃()) + 3)),F₁()) by A12, A6, SCMPDS_6:11 ;
set m3 = (LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1;
set s4 = Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),1);
set P4 = F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())));
set b = DataLoc ((F₁() . F₄()),F₅());
A14: card (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))) = (card F₃()) + 1 by SCMP_GCD:4;
set s6 = Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1));
set P6 = F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())));
set s5 = Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),1)),(LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())));
set l1 = (card (F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))))) + 1;
set P5 = F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())));
(card F₃()) + 2 < (card F₃()) + 3 by XREAL_1:6;
then A15: (card (F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))))) + 1 in dom (for-down (F₄(),F₅(),F₆(),F₃())) by A14, SCMPDS_7:42;
A16: Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1)) = Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),1)),(LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁()))) by EXTPRO_1:4;
for x being Int_position holds F₁() . x = (Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),1)) . x by A13, SCMPDS_2:56;
then A17: DataPart F₁() = DataPart (Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),1)) by SCMPDS_4:8;
A18: IC F₁() = 0 by MEMSTR_0:def 12;
A19: stop (for-down (F₄(),F₅(),F₆(),F₃())) c= F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃()))) by FUNCT_4:25;
A20: for-down (F₄(),F₅(),F₆(),F₃()) c= stop (for-down (F₄(),F₅(),F₆(),F₃())) by AFINSQ_1:74;
then A21: for-down (F₄(),F₅(),F₆(),F₃()) c= F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃()))) by A19, XBOOLE_1:1;
Shift ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),1) c= for-down (F₄(),F₅(),F₆(),F₃()) by Lm3;
then Shift ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),1) c= stop (for-down (F₄(),F₅(),F₆(),F₃())) by A20, XBOOLE_1:1;
then A22: Shift ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),1) c= F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃()))) by A19, XBOOLE_1:1;
set m0 = LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁());
set m4 = ((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1) + 1;
set s7 = Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),(((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1) + 1));
A23: IC (Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),1)) = (IC F₁()) + 1 by A2, A13, SCMPDS_2:56
.= 0 + 1 by A18 ;
then A24: IC (Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),1)),(LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())))) = (card (F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))))) + 1 by A5, A11, A8, A17, A22, SCMPDS_7:18;
then A25: CurInstr ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1)))) = (F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))) . ((card (F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))))) + 1) by A16, PBOOLE:143
.= (for-down (F₄(),F₅(),F₆(),F₃())) . ((card (F₃() ';' (AddTo (F₄(),F₅(),(- F₆()))))) + 1) by A15, A21, GRFUNC_1:2
.= goto (- ((card F₃()) + 2)) by A14, SCMPDS_7:43 ;
A26: Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),(((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1) + 1)) = Following ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1)))) by EXTPRO_1:3
.= Exec ((goto (- ((card F₃()) + 2))),(Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1)))) by A25 ;
A27: DataPart (Comput ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁(),(LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())))) = DataPart (Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),1)),(LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())))) by A5, A11, A8, A23, A17, A22, SCMPDS_7:18;

now :: thesis: for x being Int_position holds (Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),(((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1) + 1))) . x = (Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))) . x

let x be Int_position; :: thesis: (Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),(((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1) + 1))) . x = (Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))) . x
not x in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;
then A28: (Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))) . x = (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())) . x by FUNCT_4:11;
(Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),1)),(LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())))) . x = (Comput ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁(),(LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())))) . x by A27, SCMPDS_4:8
.= (Result ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) . x by A10, EXTPRO_1:23
.= (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())) . x by SCMPDS_4:def 5 ;
hence (Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),(((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1) + 1))) . x = (Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))) . x by A16, A26, A28, SCMPDS_2:54; :: thesis: verum

end;

then A29: DataPart (Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),(((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1) + 1))) = DataPart (Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))) by SCMPDS_4:8;
A30: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P₁[t] & t . F₄() = F₁() . F₄() & t . (DataLoc ((F₁() . F₄()),F₅())) > 0 holds
( (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),Q,t)) . F₄() = t . F₄() & (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),Q,t)) . (DataLoc ((F₁() . F₄()),F₅())) = (t . (DataLoc ((F₁() . F₄()),F₅()))) - F₆() & F₃() is_closed_on t,Q & F₃() is_halting_on t,Q & P₁[ Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),Q,t))] ) by A4;
A31: P₁[F₁()] by A3;
( for-down (F₄(),F₅(),F₆(),F₃()) is_closed_on F₁(),F₂() & for-down (F₄(),F₅(),F₆(),F₃()) is_halting_on F₁(),F₂() ) from SCPISORT:sch 1(A1, A31, A30);
then A32: F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃()))) halts_on F₁() by A6, SCMPDS_6:def 3;
set Es = IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁());
set bj = DataLoc (((Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))) . F₄()),F₅());
(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))) . F₄() = (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())) . F₄() by SCMPDS_5:15
.= F₁() . F₄() by A2, A3, A4 ;
then A33: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P₁[t] & t . F₄() = (Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))) . F₄() & t . (DataLoc (((Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))) . F₄()),F₅())) > 0 holds
( (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),Q,t)) . F₄() = t . F₄() & (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),Q,t)) . (DataLoc (((Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))) . F₄()),F₅())) = (t . (DataLoc (((Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))) . F₄()),F₅()))) - F₆() & F₃() is_closed_on t,Q & F₃() is_halting_on t,Q & P₁[ Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),Q,t))] ) by A4;
A34: P₁[ Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))] by A2, A3, A4;
( for-down (F₄(),F₅(),F₆(),F₃()) is_closed_on Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())),F₂() & for-down (F₄(),F₅(),F₆(),F₃()) is_halting_on Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())),F₂() ) from SCPISORT:sch 1(A1, A34, A33);
then A35: F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃()))) halts_on Initialize (Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))) by SCMPDS_6:def 3;
IC (Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),(((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1) + 1))) = ICplusConst ((Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 1))),(0 - ((card F₃()) + 2))) by A26, SCMPDS_2:54
.= 0 by A14, A24, A16, SCMPDS_7:1 ;
then A36: IC (Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))) = IC (Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 2))) by MEMSTR_0:47;
A37: Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 2)) = Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())) by A29, A36, MEMSTR_0:78;
then CurInstr ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 2)))) = (F₄(),F₅()) <=0_goto ((card F₃()) + 3) by A12, SCMPDS_6:11;
then LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁()) > (LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 2 by A32, EXTPRO_1:36, SCMPDS_6:17;
then consider nn being Nat such that
A38: LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁()) = ((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 2) + nn by NAT_1:10;
reconsider nn = nn as Nat ;
Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),(((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 2) + (LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))))))) = Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))),(LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())))))) by A37, EXTPRO_1:4;
then CurInstr ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),(((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 2) + (LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))))))))) = halt SCMPDS by A35, EXTPRO_1:def 15;
then ((LifeSpan ((F₂() +* (stop (F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))))),F₁())) + 2) + (LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))))) >= LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁()) by A32, EXTPRO_1:def 15;
then A39: LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())))) >= nn by A38, XREAL_1:6;
A40: Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁(),(LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁()))) = Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))),nn) by A37, A38, EXTPRO_1:4;
then CurInstr ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))),nn))) = halt SCMPDS by A32, EXTPRO_1:def 15;
then nn >= LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())))) by A35, EXTPRO_1:def 15;
then nn = LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())))) by A39, XXREAL_0:1;
then Result ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),F₁()) = Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))),(LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())))))) by A32, A40, EXTPRO_1:23;
hence IExec ((for-down (F₄(),F₅(),F₆(),F₃())),F₂(),F₁()) = Comput ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁()))),(LifeSpan ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())))))) by SCMPDS_4:def 5
.= Result ((F₂() +* (stop (for-down (F₄(),F₅(),F₆(),F₃())))),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())))) by A35, EXTPRO_1:23
.= IExec ((for-down (F₄(),F₅(),F₆(),F₃())),F₂(),(Initialize (IExec ((F₃() ';' (AddTo (F₄(),F₅(),(- F₆())))),F₂(),F₁())))) by SCMPDS_4:def 5 ;
:: thesis: verum