A5:
Initialize F_{2}() = F_{2}()
by MEMSTR_0:44;

set WHL = while<0 (F_{5}(),F_{6}(),F_{4}());

set pWHL = stop (while<0 (F_{5}(),F_{6}(),F_{4}()));

set P1 = F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())));

set PI = F_{3}() +* (stop F_{4}());

set m1 = (LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 2;

set s2 = Initialize (IExec (F_{4}(),F_{3}(),F_{2}()));

set P2 = F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())));

set m2 = LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))));

A6: P_{1}[F_{2}()]
by A3;

A7: stop F_{4}() c= F_{3}() +* (stop F_{4}())
by FUNCT_4:25;

A8: F_{4}() is_closed_on F_{2}(),F_{3}() +* (stop F_{4}())
by A1, A3, A4;

F_{4}() is_halting_on F_{2}(),F_{3}()
by A1, A3, A4;

then A9: F_{3}() +* (stop F_{4}()) halts_on F_{2}()
by A5, SCMPDS_6:def 3;

(F_{3}() +* (stop F_{4}())) +* (stop F_{4}()) halts_on F_{2}()
by A9;

then A10: F_{4}() is_halting_on F_{2}(),F_{3}() +* (stop F_{4}())
by A5, SCMPDS_6:def 3;

set Es = IExec (F_{4}(),F_{3}(),F_{2}());

set bj = DataLoc (((Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))) . F_{5}()),F_{6}());

set EP = F_{3}();

A11: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st P_{1}[t] & t . F_{5}() = F_{2}() . F_{5}() & t . (DataLoc ((F_{2}() . F_{5}()),F_{6}())) < 0 holds

( (IExec (F_{4}(),Q,t)) . F_{5}() = t . F_{5}() & F_{4}() is_closed_on t,Q & F_{4}() is_halting_on t,Q & F_{1}((Initialize (IExec (F_{4}(),Q,t)))) < F_{1}(t) & P_{1}[ Initialize (IExec (F_{4}(),Q,t))] )
by A4;

A12: for t being 0 -started State of SCMPDS st P_{1}[t] & F_{1}(t) = 0 holds

t . (DataLoc ((F_{2}() . F_{5}()),F_{6}())) >= 0
by A2;

( while<0 (F_{5}(),F_{6}(),F_{4}()) is_closed_on F_{2}(),F_{3}() & while<0 (F_{5}(),F_{6}(),F_{4}()) is_halting_on F_{2}(),F_{3}() )
from SCMPDS_8:sch 1(A12, A6, A11);

then A13: F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}()))) halts_on F_{2}()
by A5, SCMPDS_6:def 3;

A14: (IExec (F_{4}(),F_{3}(),F_{2}())) . F_{5}() = (Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))) . F_{5}()
by SCMPDS_5:15;

A15: (IExec (F_{4}(),F_{3}(),F_{2}())) . F_{5}() = F_{2}() . F_{5}()
by A1, A3, A4;

then A16: for t being 0 -started State of SCMPDS st P_{1}[t] & F_{1}(t) = 0 holds

t . (DataLoc (((Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))) . F_{5}()),F_{6}())) >= 0
by A2, A14;

A17: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st P_{1}[t] & t . F_{5}() = (Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))) . F_{5}() & t . (DataLoc (((Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))) . F_{5}()),F_{6}())) < 0 holds

( (IExec (F_{4}(),Q,t)) . F_{5}() = t . F_{5}() & F_{4}() is_closed_on t,Q & F_{4}() is_halting_on t,Q & F_{1}((Initialize (IExec (F_{4}(),Q,t)))) < F_{1}(t) & P_{1}[ Initialize (IExec (F_{4}(),Q,t))] )
by A4, A15, A14;

A18: P_{1}[ Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))]
by A1, A3, A4;

( while<0 (F_{5}(),F_{6}(),F_{4}()) is_closed_on Initialize (IExec (F_{4}(),F_{3}(),F_{2}())),F_{3}() & while<0 (F_{5}(),F_{6}(),F_{4}()) is_halting_on Initialize (IExec (F_{4}(),F_{3}(),F_{2}())),F_{3}() )
from SCMPDS_8:sch 1(A16, A18, A17);

then A19: F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}()))) halts_on Initialize (Initialize (IExec (F_{4}(),F_{3}(),F_{2}())))
by SCMPDS_6:def 3;

set s4 = Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),1);

set P4 = F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())));

set i1 = (F_{5}(),F_{6}()) >=0_goto ((card F_{4}()) + 2);

set i2 = goto (- ((card F_{4}()) + 1));

set b = DataLoc ((F_{2}() . F_{5}()),F_{6}());

A20: while<0 (F_{5}(),F_{6}(),F_{4}()) = ((F_{5}(),F_{6}()) >=0_goto ((card F_{4}()) + 2)) ';' (F_{4}() ';' (goto (- ((card F_{4}()) + 1))))
by SCMPDS_4:15;

set mI = LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}());

set s5 = Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),1)),(LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())));

set P5 = F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())));

set l1 = (card F_{4}()) + 1;

A21: IC F_{2}() = 0
by MEMSTR_0:def 11;

A22: Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),(0 + 1)) =
Following ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),0)))
by EXTPRO_1:3

.= Following ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}())

.= Exec (((F_{5}(),F_{6}()) >=0_goto ((card F_{4}()) + 2)),F_{2}())
by A20, A5, SCMPDS_6:11
;

for a being Int_position holds F_{2}() . a = (Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),1)) . a
by A22, SCMPDS_2:57;

then A23: DataPart F_{2}() = DataPart (Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),1))
by SCMPDS_4:8;

set m3 = (LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1;

set s6 = Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1));

set P6 = F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())));

(card F_{4}()) + 1 < (card F_{4}()) + 2
by XREAL_1:6;

then A24: (card F_{4}()) + 1 in dom (while<0 (F_{5}(),F_{6}(),F_{4}()))
by Th5;

set m0 = LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}());

set s7 = Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),(((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1) + 1));

A25: while<0 (F_{5}(),F_{6}(),F_{4}()) c= stop (while<0 (F_{5}(),F_{6}(),F_{4}()))
by AFINSQ_1:74;

stop (while<0 (F_{5}(),F_{6}(),F_{4}())) c= F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))
by FUNCT_4:25;

then A26: while<0 (F_{5}(),F_{6}(),F_{4}()) c= F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))
by A25, XBOOLE_1:1;

Shift (F_{4}(),1) c= while<0 (F_{5}(),F_{6}(),F_{4}())
by Lm2;

then A27: Shift (F_{4}(),1) c= F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))
by A26, XBOOLE_1:1;

A28: IC (Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),1)) =
(IC F_{2}()) + 1
by A1, A22, SCMPDS_2:57

.= 0 + 1 by A21 ;

then A29: IC (Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),1)),(LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())))) = (card F_{4}()) + 1
by A7, A10, A8, A23, A27, SCMPDS_7:18;

A30: (F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))) /. (IC (Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1)))) = (F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))) . (IC (Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1))))
by PBOOLE:143;

A31: Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1)) = Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),1)),(LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())))
by EXTPRO_1:4;

then A32: CurInstr ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1)))) =
(F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))) . ((card F_{4}()) + 1)
by A7, A10, A8, A28, A23, A27, A30, SCMPDS_7:18

.= (while<0 (F_{5}(),F_{6}(),F_{4}())) . ((card F_{4}()) + 1)
by A24, A26, GRFUNC_1:2

.= goto (- ((card F_{4}()) + 1))
by Th6
;

A33: Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),(((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1) + 1)) =
Following ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1))))
by EXTPRO_1:3

.= Exec ((goto (- ((card F_{4}()) + 1))),(Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1))))
by A32
;

then IC (Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),(((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1) + 1))) =
ICplusConst ((Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1))),(0 - ((card F_{4}()) + 1)))
by SCMPDS_2:54

.= 0 by A29, A31, SCMPDS_7:1 ;

then A34: IC (Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))) = IC (Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 2)))
by MEMSTR_0:def 11;

A35: DataPart (Comput ((F_{3}() +* (stop F_{4}())),F_{2}(),(LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())))) = DataPart (Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),1)),(LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}()))))
by A7, A10, A8, A28, A23, A27, SCMPDS_7:18;

_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),(((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1) + 1))) = DataPart (Initialize (IExec (F_{4}(),F_{3}(),F_{2}())))
by SCMPDS_4:8;

A38: Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 2)) = Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))
by A37, A34, MEMSTR_0:78;

then CurInstr ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 2)))) = (F_{5}(),F_{6}()) >=0_goto ((card F_{4}()) + 2)
by A20, SCMPDS_6:11;

then LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}()) > (LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 2
by A13, EXTPRO_1:36, SCMPDS_6:18;

then consider nn being Nat such that

A39: LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}()) = ((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 2) + nn
by NAT_1:10;

reconsider nn = nn as Nat ;

Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),(((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 2) + (LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))))))) = Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))),(LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))))))
by A38, EXTPRO_1:4;

then CurInstr ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),(((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 2) + (LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))))))))) = halt SCMPDS
by A19, EXTPRO_1:def 15;

then ((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 2) + (LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))))) >= LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}())
by A13, EXTPRO_1:def 15;

then A40: LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}())))) >= nn
by A39, XREAL_1:6;

A41: Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),(LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}()))) = Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))),nn)
by A38, A39, EXTPRO_1:4;

then CurInstr ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))),nn))) = halt SCMPDS
by A13, EXTPRO_1:def 15;

then nn >= LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))))
by A19, EXTPRO_1:def 15;

then nn = LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))))
by A40, XXREAL_0:1;

then Result ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}()) = Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))),(LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))))))
by A13, A41, EXTPRO_1:23;

hence IExec ((while<0 (F_{5}(),F_{6}(),F_{4}())),F_{3}(),F_{2}()) =
Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))),(LifeSpan ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))))))
by SCMPDS_4:def 5

.= Result ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))))
by A19, EXTPRO_1:23

.= IExec ((while<0 (F_{5}(),F_{6}(),F_{4}())),F_{3}(),(Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))))
by SCMPDS_4:def 5
;

:: thesis: verum

set WHL = while<0 (F

set pWHL = stop (while<0 (F

set P1 = F

set PI = F

set m1 = (LifeSpan ((F

set s2 = Initialize (IExec (F

set P2 = F

set m2 = LifeSpan ((F

A6: P

A7: stop F

A8: F

F

then A9: F

(F

then A10: F

set Es = IExec (F

set bj = DataLoc (((Initialize (IExec (F

set EP = F

A11: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st P

( (IExec (F

A12: for t being 0 -started State of SCMPDS st P

t . (DataLoc ((F

( while<0 (F

then A13: F

A14: (IExec (F

A15: (IExec (F

then A16: for t being 0 -started State of SCMPDS st P

t . (DataLoc (((Initialize (IExec (F

A17: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st P

( (IExec (F

A18: P

( while<0 (F

then A19: F

set s4 = Comput ((F

set P4 = F

set i1 = (F

set i2 = goto (- ((card F

set b = DataLoc ((F

A20: while<0 (F

set mI = LifeSpan ((F

set s5 = Comput ((F

set P5 = F

set l1 = (card F

A21: IC F

A22: Comput ((F

.= Following ((F

.= Exec (((F

for a being Int_position holds F

then A23: DataPart F

set m3 = (LifeSpan ((F

set s6 = Comput ((F

set P6 = F

(card F

then A24: (card F

set m0 = LifeSpan ((F

set s7 = Comput ((F

A25: while<0 (F

stop (while<0 (F

then A26: while<0 (F

Shift (F

then A27: Shift (F

A28: IC (Comput ((F

.= 0 + 1 by A21 ;

then A29: IC (Comput ((F

A30: (F

A31: Comput ((F

then A32: CurInstr ((F

.= (while<0 (F

.= goto (- ((card F

A33: Comput ((F

.= Exec ((goto (- ((card F

then IC (Comput ((F

.= 0 by A29, A31, SCMPDS_7:1 ;

then A34: IC (Initialize (IExec (F

A35: DataPart (Comput ((F

now :: thesis: for x being Int_position holds (Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),(((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1) + 1))) . x = (Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))) . x

then A37:
DataPart (Comput ((Flet x be Int_position; :: thesis: (Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),(((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1) + 1))) . x = (Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))) . x

A36: not x in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;

(Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),(Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),1)),(LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())))) . x =
(Comput ((F_{3}() +* (stop F_{4}())),F_{2}(),(LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())))) . x
by A35, SCMPDS_4:8

.= (Result ((F_{3}() +* (stop F_{4}())),F_{2}())) . x
by A9, EXTPRO_1:23

.= (IExec (F_{4}(),F_{3}(),F_{2}())) . x
by SCMPDS_4:def 5
;

hence (Comput ((F_{3}() +* (stop (while<0 (F_{5}(),F_{6}(),F_{4}())))),F_{2}(),(((LifeSpan ((F_{3}() +* (stop F_{4}())),F_{2}())) + 1) + 1))) . x =
(IExec (F_{4}(),F_{3}(),F_{2}())) . x
by A31, A33, SCMPDS_2:54

.= (Initialize (IExec (F_{4}(),F_{3}(),F_{2}()))) . x
by A36, FUNCT_4:11
;

:: thesis: verum

end;A36: not x in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;

(Comput ((F

.= (Result ((F

.= (IExec (F

hence (Comput ((F

.= (Initialize (IExec (F

:: thesis: verum

A38: Comput ((F

then CurInstr ((F

then LifeSpan ((F

then consider nn being Nat such that

A39: LifeSpan ((F

reconsider nn = nn as Nat ;

Comput ((F

then CurInstr ((F

then ((LifeSpan ((F

then A40: LifeSpan ((F

A41: Comput ((F

then CurInstr ((F

then nn >= LifeSpan ((F

then nn = LifeSpan ((F

then Result ((F

hence IExec ((while<0 (F

.= Result ((F

.= IExec ((while<0 (F

:: thesis: verum