set i1 = (F4(),F5()) <=0_goto ((card F3()) + 3);
set J = F3() ';' (AddTo (F4(),F5(),(- F6())));
set i3 = goto (- ((card F3()) + 2));
set FOR = for-down (F4(),F5(),F6(),F3());
set pFOR = stop (for-down (F4(),F5(),F6(),F3()));
set P1 = F2() +* (stop (for-down (F4(),F5(),F6(),F3())));
set PJ = F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))));
set mJ = LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1());
set m1 = (LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 2;
set s2 = Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()));
set m2 = LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))));
A5:
stop (F3() ';' (AddTo (F4(),F5(),(- F6())))) c= F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))
by FUNCT_4:25;
A6:
Initialize F1() = F1()
by MEMSTR_0:44;
A7:
( F3() is_closed_on F1(),F2() & F3() is_halting_on F1(),F2() )
by A2, A3, A4;
then
F3() ';' (AddTo (F4(),F5(),(- F6()))) is_closed_on F1(),F2()
by Th5;
then A8:
F3() ';' (AddTo (F4(),F5(),(- F6()))) is_closed_on F1(),F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))
by A6, SCMPDS_6:24;
A9:
F3() ';' (AddTo (F4(),F5(),(- F6()))) is_halting_on F1(),F2()
by A7, Th5;
then A10:
F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6()))))) halts_on F1()
by A6, SCMPDS_6:def 3;
(F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))) +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6()))))) halts_on Initialize F1()
by A9, SCMPDS_6:def 3;
then A11:
F3() ';' (AddTo (F4(),F5(),(- F6()))) is_halting_on F1(),F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))
by SCMPDS_6:def 3;
A12:
for-down (F4(),F5(),F6(),F3()) = ((F4(),F5()) <=0_goto ((card F3()) + 3)) ';' ((F3() ';' (AddTo (F4(),F5(),(- F6())))) ';' (goto (- ((card F3()) + 2))))
by Lm2;
A13: Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),(0 + 1)) =
Following ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),0)))
by EXTPRO_1:3
.=
Following ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1())
by EXTPRO_1:2
.=
Exec (((F4(),F5()) <=0_goto ((card F3()) + 3)),F1())
by A12, A6, SCMPDS_6:11
;
set m3 = (LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1;
set s4 = Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),1);
set P4 = F2() +* (stop (for-down (F4(),F5(),F6(),F3())));
set b = DataLoc ((F1() . F4()),F5());
A14:
card (F3() ';' (AddTo (F4(),F5(),(- F6())))) = (card F3()) + 1
by SCMP_GCD:4;
set s6 = Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1));
set P6 = F2() +* (stop (for-down (F4(),F5(),F6(),F3())));
set s5 = Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),1)),(LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())));
set l1 = (card (F3() ';' (AddTo (F4(),F5(),(- F6()))))) + 1;
set P5 = F2() +* (stop (for-down (F4(),F5(),F6(),F3())));
(card F3()) + 2 < (card F3()) + 3
by XREAL_1:6;
then A15:
(card (F3() ';' (AddTo (F4(),F5(),(- F6()))))) + 1 in dom (for-down (F4(),F5(),F6(),F3()))
by A14, SCMPDS_7:42;
A16:
Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1)) = Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),1)),(LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())))
by EXTPRO_1:4;
for x being Int_position holds F1() . x = (Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),1)) . x
by A13, SCMPDS_2:56;
then A17:
DataPart F1() = DataPart (Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),1))
by SCMPDS_4:8;
A18:
IC F1() = 0
by MEMSTR_0:def 12;
A19:
stop (for-down (F4(),F5(),F6(),F3())) c= F2() +* (stop (for-down (F4(),F5(),F6(),F3())))
by FUNCT_4:25;
A20:
for-down (F4(),F5(),F6(),F3()) c= stop (for-down (F4(),F5(),F6(),F3()))
by AFINSQ_1:74;
then A21:
for-down (F4(),F5(),F6(),F3()) c= F2() +* (stop (for-down (F4(),F5(),F6(),F3())))
by A19, XBOOLE_1:1;
Shift ((F3() ';' (AddTo (F4(),F5(),(- F6())))),1) c= for-down (F4(),F5(),F6(),F3())
by Lm3;
then
Shift ((F3() ';' (AddTo (F4(),F5(),(- F6())))),1) c= stop (for-down (F4(),F5(),F6(),F3()))
by A20, XBOOLE_1:1;
then A22:
Shift ((F3() ';' (AddTo (F4(),F5(),(- F6())))),1) c= F2() +* (stop (for-down (F4(),F5(),F6(),F3())))
by A19, XBOOLE_1:1;
set m0 = LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1());
set m4 = ((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1) + 1;
set s7 = Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),(((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1) + 1));
A23: IC (Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),1)) =
(IC F1()) + 1
by A2, A13, SCMPDS_2:56
.=
0 + 1
by A18
;
then A24:
IC (Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),1)),(LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())))) = (card (F3() ';' (AddTo (F4(),F5(),(- F6()))))) + 1
by A5, A11, A8, A17, A22, SCMPDS_7:18;
then A25: CurInstr ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1)))) =
(F2() +* (stop (for-down (F4(),F5(),F6(),F3())))) . ((card (F3() ';' (AddTo (F4(),F5(),(- F6()))))) + 1)
by A16, PBOOLE:143
.=
(for-down (F4(),F5(),F6(),F3())) . ((card (F3() ';' (AddTo (F4(),F5(),(- F6()))))) + 1)
by A15, A21, GRFUNC_1:2
.=
goto (- ((card F3()) + 2))
by A14, SCMPDS_7:43
;
A26: Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),(((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1) + 1)) =
Following ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1))))
by EXTPRO_1:3
.=
Exec ((goto (- ((card F3()) + 2))),(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1))))
by A25
;
A27:
DataPart (Comput ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1(),(LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())))) = DataPart (Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),1)),(LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1()))))
by A5, A11, A8, A23, A17, A22, SCMPDS_7:18;
now for x being Int_position holds (Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),(((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1) + 1))) . x = (Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))) . xlet x be
Int_position;
(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),(((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1) + 1))) . x = (Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))) . x
not
x in dom (Start-At (0,SCMPDS))
by SCMPDS_4:18;
then A28:
(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))) . x = (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1())) . x
by FUNCT_4:11;
(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),1)),(LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())))) . x =
(Comput ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1(),(LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())))) . x
by A27, SCMPDS_4:8
.=
(Result ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) . x
by A10, EXTPRO_1:23
.=
(IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1())) . x
by SCMPDS_4:def 5
;
hence
(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),(((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1) + 1))) . x = (Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))) . x
by A16, A26, A28, SCMPDS_2:54;
verum end;
then A29:
DataPart (Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),(((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1) + 1))) = DataPart (Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1())))
by SCMPDS_4:8;
A30:
for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F4() = F1() . F4() & t . (DataLoc ((F1() . F4()),F5())) > 0 holds
( (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . F4() = t . F4() & (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . (DataLoc ((F1() . F4()),F5())) = (t . (DataLoc ((F1() . F4()),F5()))) - F6() & F3() is_closed_on t,Q & F3() is_halting_on t,Q & P1[ Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t))] )
by A4;
A31:
P1[F1()]
by A3;
( for-down (F4(),F5(),F6(),F3()) is_closed_on F1(),F2() & for-down (F4(),F5(),F6(),F3()) is_halting_on F1(),F2() )
from SCPISORT:sch 1(A1, A31, A30);
then A32:
F2() +* (stop (for-down (F4(),F5(),F6(),F3()))) halts_on F1()
by A6, SCMPDS_6:def 3;
set Es = IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1());
set bj = DataLoc (((Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))) . F4()),F5());
(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))) . F4() =
(IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1())) . F4()
by SCMPDS_5:15
.=
F1() . F4()
by A2, A3, A4
;
then A33:
for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F4() = (Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))) . F4() & t . (DataLoc (((Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))) . F4()),F5())) > 0 holds
( (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . F4() = t . F4() & (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . (DataLoc (((Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))) . F4()),F5())) = (t . (DataLoc (((Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))) . F4()),F5()))) - F6() & F3() is_closed_on t,Q & F3() is_halting_on t,Q & P1[ Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t))] )
by A4;
A34:
P1[ Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))]
by A2, A3, A4;
( for-down (F4(),F5(),F6(),F3()) is_closed_on Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1())),F2() & for-down (F4(),F5(),F6(),F3()) is_halting_on Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1())),F2() )
from SCPISORT:sch 1(A1, A34, A33);
then A35:
F2() +* (stop (for-down (F4(),F5(),F6(),F3()))) halts_on Initialize (Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1())))
by SCMPDS_6:def 3;
IC (Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),(((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1) + 1))) =
ICplusConst ((Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 1))),(0 - ((card F3()) + 2)))
by A26, SCMPDS_2:54
.=
0
by A14, A24, A16, SCMPDS_7:1
;
then A36:
IC (Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))) = IC (Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 2)))
by MEMSTR_0:47;
A37:
Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 2)) = Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))
by A29, A36, MEMSTR_0:78;
then
CurInstr ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 2)))) = (F4(),F5()) <=0_goto ((card F3()) + 3)
by A12, SCMPDS_6:11;
then
LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1()) > (LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 2
by A32, EXTPRO_1:36, SCMPDS_6:17;
then consider nn being Nat such that
A38:
LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1()) = ((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 2) + nn
by NAT_1:10;
reconsider nn = nn as Nat ;
Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),(((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 2) + (LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))))))) = Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))),(LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))))))
by A37, EXTPRO_1:4;
then
CurInstr ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),(((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 2) + (LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))))))))) = halt SCMPDS
by A35, EXTPRO_1:def 15;
then
((LifeSpan ((F2() +* (stop (F3() ';' (AddTo (F4(),F5(),(- F6())))))),F1())) + 2) + (LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))))) >= LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1())
by A32, EXTPRO_1:def 15;
then A39:
LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1())))) >= nn
by A38, XREAL_1:6;
A40:
Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1(),(LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1()))) = Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))),nn)
by A37, A38, EXTPRO_1:4;
then
CurInstr ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))),nn))) = halt SCMPDS
by A32, EXTPRO_1:def 15;
then
nn >= LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))))
by A35, EXTPRO_1:def 15;
then
nn = LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))))
by A39, XXREAL_0:1;
then
Result ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),F1()) = Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))),(LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))))))
by A32, A40, EXTPRO_1:23;
hence IExec ((for-down (F4(),F5(),F6(),F3())),F2(),F1()) =
Comput ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))),(LifeSpan ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))))))
by SCMPDS_4:def 5
.=
Result ((F2() +* (stop (for-down (F4(),F5(),F6(),F3())))),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))))
by A35, EXTPRO_1:23
.=
IExec ((for-down (F4(),F5(),F6(),F3())),F2(),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))))
by SCMPDS_4:def 5
;
verum