A5: Initialize F₂() = F₂() by MEMSTR_0:44;
set WHL = while<>0 (F₅(),F₆(),F₄());
set s1 = F₂();
set P1 = F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())));
set sI = F₂();
set PI = F₃() +* (stop F₄());
set m1 = (LifeSpan ((F₃() +* (stop F₄())),F₂())) + 2;
set s2 = Initialize (IExec (F₄(),F₃(),F₂()));
set m2 = LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))));
A6: stop F₄() c= F₃() +* (stop F₄()) by FUNCT_4:25;
F₄() is_closed_on F₂(),F₃() by A1, A3, A4;
then A7: F₄() is_closed_on F₂(),F₃() +* (stop F₄()) by A5, SCMPDS_6:24;
F₄() is_halting_on F₂(),F₃() by A1, A3, A4;
then A8: F₃() +* (stop F₄()) halts_on F₂() by A5, SCMPDS_6:def 3;
(F₃() +* (stop F₄())) +* (stop F₄()) halts_on Initialize F₂() by A8, A5;
then A9: F₄() is_halting_on F₂(),F₃() +* (stop F₄()) by SCMPDS_6:def 3;
set s4 = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),1);
set P4 = F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())));
set i1 = (F₅(),F₆()) <>0_goto 2;
set i2 = goto ((card F₄()) + 2);
set i3 = goto (- ((card F₄()) + 2));
set b = DataLoc ((F₂() . F₅()),F₆());
A10: IC F₂() = 0 by A5, MEMSTR_0:47;
set mI = LifeSpan ((F₃() +* (stop F₄())),F₂());
set s5 = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),1)),(LifeSpan ((F₃() +* (stop F₄())),F₂())));
set P5 = F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())));
set l2 = (card F₄()) + 2;
A11: while<>0 (F₅(),F₆(),F₄()) = ((F₅(),F₆()) <>0_goto 2) ';' (((goto ((card F₄()) + 2)) ';' F₄()) ';' (goto (- ((card F₄()) + 2)))) by Lm8;
set m3 = (LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1;
set s6 = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1));
set P6 = F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())));
(card F₄()) + 2 < (card F₄()) + 3 by XREAL_1:6;
then A12: (card F₄()) + 2 in dom (while<>0 (F₅(),F₆(),F₄())) by Th9;
set s7 = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),(((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1) + 1));
set P7 = F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())));
A13: IExec (F₄(),F₃(),F₂()) = Result ((F₃() +* (stop F₄())),F₂()) by SCMPDS_4:def 5;
A14: stop (while<>0 (F₅(),F₆(),F₄())) c= F₃() +* (stop (while<>0 (F₅(),F₆(),F₄()))) by FUNCT_4:25;
while<>0 (F₅(),F₆(),F₄()) c= stop (while<>0 (F₅(),F₆(),F₄())) by AFINSQ_1:74;
then A15: while<>0 (F₅(),F₆(),F₄()) c= F₃() +* (stop (while<>0 (F₅(),F₆(),F₄()))) by A14, XBOOLE_1:1;
deffunc H₁( State of SCMPDS) -> Element of NAT = F₁($1);
A16: for t being 0 -started State of SCMPDS st P₁[t] & H₁(t) = 0 holds
t . (DataLoc ((F₂() . F₅()),F₆())) = 0 by A2;
A17: 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₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & H₁( Initialize (IExec (F₄(),Q,t))) < H₁(t) & P₁[ Initialize (IExec (F₄(),Q,t))] ) by A4;
A18: Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),(0 + 1)) = Following ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),0))) by EXTPRO_1:3
.= Following ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂())
.= Exec (((F₅(),F₆()) <>0_goto 2),F₂()) by A11, A5, SCMPDS_6:11 ;
Shift (F₄(),2) c= while<>0 (F₅(),F₆(),F₄()) by Lm9;
then Shift (F₄(),2) c= F₃() +* (stop (while<>0 (F₅(),F₆(),F₄()))) by A15, XBOOLE_1:1;
then A19: Shift (F₄(),2) c= F₃() +* (stop (while<>0 (F₅(),F₆(),F₄()))) ;
for a being Int_position holds F₂() . a = (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),1)) . a by A18, SCMPDS_2:55;
then A20: DataPart F₂() = DataPart (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),1)) by SCMPDS_4:8;
A21: IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),1)) = ICplusConst (F₂(),2) by A1, A18, SCMPDS_2:55
.= 0 + 2 by A10, SCMPDS_6:12 ;
then A22: IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),1)),(LifeSpan ((F₃() +* (stop F₄())),F₂())))) = (card F₄()) + 2 by A6, A9, A7, A20, A19, SCMPDS_7:18;
A23: (F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))) /. (IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1)))) = (F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))) . (IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1)))) by PBOOLE:143;
A24: Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1)) = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),1)),(LifeSpan ((F₃() +* (stop F₄())),F₂()))) by EXTPRO_1:4;
then A25: CurInstr ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1)))) = (F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))) . ((card F₄()) + 2) by A6, A9, A7, A21, A20, A19, A23, SCMPDS_7:18
.= (F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))) . ((card F₄()) + 2)
.= (F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))) . ((card F₄()) + 2)
.= (while<>0 (F₅(),F₆(),F₄())) . ((card F₄()) + 2) by A12, A15, GRFUNC_1:2
.= goto (- ((card F₄()) + 2)) by Th11 ;
A26: Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),(((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1) + 1)) = Following ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1)))) by EXTPRO_1:3
.= Exec ((goto (- ((card F₄()) + 2))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1)))) by A25 ;
then IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),(((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1) + 1))) = ICplusConst ((Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1))),(0 - ((card F₄()) + 2))) by SCMPDS_2:54
.= 0 by A22, A24, SCMPDS_7:1 ;
then A27: IC (Initialize (IExec (F₄(),F₃(),F₂()))) = IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 2))) by MEMSTR_0:47;
A28: DataPart (Comput ((F₃() +* (stop F₄())),F₂(),(LifeSpan ((F₃() +* (stop F₄())),F₂())))) = DataPart (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),1)),(LifeSpan ((F₃() +* (stop F₄())),F₂())))) by A6, A9, A7, A21, A20, A19, SCMPDS_7:18;

now :: thesis: for x being Int_position holds (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),(((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1) + 1))) . x = (Initialize (IExec (F₄(),F₃(),F₂()))) . x

let x be Int_position; :: thesis: (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),(((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1) + 1))) . x = (Initialize (IExec (F₄(),F₃(),F₂()))) . x
A29: not x in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;
(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),1)),(LifeSpan ((F₃() +* (stop F₄())),F₂())))) . x = (Comput ((F₃() +* (stop F₄())),F₂(),(LifeSpan ((F₃() +* (stop F₄())),F₂())))) . x by A28, SCMPDS_4:8
.= (Result ((F₃() +* (stop F₄())),F₂())) . x by A8, EXTPRO_1:23
.= (IExec (F₄(),F₃(),F₂())) . x by A13 ;
hence (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),(((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1) + 1))) . x = (IExec (F₄(),F₃(),F₂())) . x by A24, A26, SCMPDS_2:54
.= (Initialize (IExec (F₄(),F₃(),F₂()))) . x by A29, FUNCT_4:11 ;
:: thesis: verum

end;

then A30: DataPart (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),(((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 1) + 1))) = DataPart (Initialize (IExec (F₄(),F₃(),F₂()))) by SCMPDS_4:8;
set m0 = LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂());
A31: P₁[F₂()] by A3;
( while<>0 (F₅(),F₆(),F₄()) is_closed_on F₂(),F₃() & while<>0 (F₅(),F₆(),F₄()) is_halting_on F₂(),F₃() ) from SCPINVAR:sch 3(A16, A31, A17);
then A32: F₃() +* (stop (while<>0 (F₅(),F₆(),F₄()))) halts_on F₂() by A5, SCMPDS_6:def 3;
deffunc H₂( State of SCMPDS) -> Element of NAT = H₁($1);
set Es = IExec (F₄(),F₃(),F₂());
set bj = DataLoc (((IExec (F₄(),F₃(),F₂())) . F₅()),F₆());
set EP = F₃();
A33: (IExec (F₄(),F₃(),F₂())) . F₅() = F₂() . F₅() by A1, A3, A4;
A34: (Initialize (IExec (F₄(),F₃(),F₂()))) . F₅() = (IExec (F₄(),F₃(),F₂())) . F₅() by SCMPDS_5:15;
A35: for t being 0 -started State of SCMPDS st P₁[t] & H₂(t) = 0 holds
t . (DataLoc (((Initialize (IExec (F₄(),F₃(),F₂()))) . F₅()),F₆())) = 0 by A2, A33, A34;
A36: P₁[ Initialize (IExec (F₄(),F₃(),F₂()))] by A1, A3, A4;
A37: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P₁[t] & t . F₅() = (Initialize (IExec (F₄(),F₃(),F₂()))) . F₅() & t . (DataLoc (((Initialize (IExec (F₄(),F₃(),F₂()))) . F₅()),F₆())) <> 0 holds
( (IExec (F₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & H₂( Initialize (IExec (F₄(),Q,t))) < H₂(t) & P₁[ Initialize (IExec (F₄(),Q,t))] ) by A4, A33, A34;
A38: ( while<>0 (F₅(),F₆(),F₄()) is_closed_on Initialize (IExec (F₄(),F₃(),F₂())),F₃() & while<>0 (F₅(),F₆(),F₄()) is_halting_on Initialize (IExec (F₄(),F₃(),F₂())),F₃() ) from SCPINVAR:sch 3(A35, A36, A37);
while<>0 (F₅(),F₆(),F₄()) is_halting_on IExec (F₄(),F₃(),F₂()),F₃()

proof

F₃() +* (stop (while<>0 (F₅(),F₆(),F₄()))) halts_on Initialize (Initialize (IExec (F₄(),F₃(),F₂()))) by A38, SCMPDS_6:def 3;
hence while<>0 (F₅(),F₆(),F₄()) is_halting_on IExec (F₄(),F₃(),F₂()),F₃() by SCMPDS_6:def 3; :: thesis: verum

end;

then A39: F₃() +* (stop (while<>0 (F₅(),F₆(),F₄()))) halts_on Initialize (IExec (F₄(),F₃(),F₂())) by SCMPDS_6:def 3;
A40: Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 2)) = Initialize (IExec (F₄(),F₃(),F₂())) by A30, A27, MEMSTR_0:78;
then CurInstr ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 2)))) = (F₅(),F₆()) <>0_goto 2 by A11, SCMPDS_6:11;
then LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂()) > (LifeSpan ((F₃() +* (stop F₄())),F₂())) + 2 by A32, EXTPRO_1:36, SCMPDS_6:16;
then consider nn being Nat such that
A41: LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂()) = ((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 2) + nn by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 12;
IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),(((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 2) + (LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂())))))))) = IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))),(LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))))))) by A40, EXTPRO_1:4;
then CurInstr ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),(((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 2) + (LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))))))))) = CurInstr ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))),(LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))))))))
.= halt SCMPDS by A39, EXTPRO_1:def 15 ;
then ((LifeSpan ((F₃() +* (stop F₄())),F₂())) + 2) + (LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))))) >= LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂()) by A32, EXTPRO_1:def 15;
then A42: LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂())))) >= nn by A41, XREAL_1:6;
A43: Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂(),(LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂()))) = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))),nn) by A40, A41, EXTPRO_1:4;
then CurInstr ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))),nn))) = halt SCMPDS by A32, EXTPRO_1:def 15;
then nn >= LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂())))) by A39, EXTPRO_1:def 15;
then nn = LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂())))) by A42, XXREAL_0:1;
then Result ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),F₂()) = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))),(LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂())))))) by A32, A43, EXTPRO_1:23;
hence IExec ((while<>0 (F₅(),F₆(),F₄())),F₃(),F₂()) = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))),(LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂())))))) by SCMPDS_4:def 5
.= Result ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂())))) by A39, EXTPRO_1:23
.= IExec ((while<>0 (F₅(),F₆(),F₄())),F₃(),(Initialize (IExec (F₄(),F₃(),F₂())))) by SCMPDS_4:def 5 ;
:: thesis: verum