set i1 = (F₅(),F₆()) >=0_goto ((card F₄()) + 2);
set i2 = goto (- ((card F₄()) + 1));
set WHL = while<0 (F₅(),F₆(),F₄());
set pWHL = stop (while<0 (F₅(),F₆(),F₄()));
set pI = stop F₄();
set b = DataLoc ((F₂() . F₅()),F₆());
defpred S₁[ Element of NAT ] means for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st F₁(t) <= $1 & P₁[t] & t . F₅() = F₂() . F₅() holds
( while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q );
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st F₁(t) <= k + 1 & P₁[t] & t . F₅() = F₂() . F₅() holds
( while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q )
let Q be Instruction-Sequence of SCMPDS; :: thesis: ( F₁(t) <= k + 1 & P₁[t] & t . F₅() = F₂() . F₅() implies ( while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q ) )
T: Initialize t = t by MEMSTR_0:44;
assume A7: F₁(t) <= k + 1 ; :: thesis: ( not P₁[t] or not t . F₅() = F₂() . F₅() or ( while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q ) )
assume A8: P₁[t] ; :: thesis: ( not t . F₅() = F₂() . F₅() or ( while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q ) )
assume A9: t . F₅() = F₂() . F₅() ; :: thesis: ( while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q )

per cases ( t . (DataLoc ((F₂() . F₅()),F₆())) >= 0 or t . (DataLoc ((F₂() . F₅()),F₆())) < 0 ) ;

suppose t . (DataLoc ((F₂() . F₅()),F₆())) >= 0 ; :: thesis: ( while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q )

hence ( while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q ) by A9, Th9; :: thesis: verum

end;

suppose A10: t . (DataLoc ((F₂() . F₅()),F₆())) < 0 ; :: thesis: ( while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q )

A14: 0 in dom (stop (while<0 (F₅(),F₆(),F₄()))) by COMPOS_1:36;
A17: while<0 (F₅(),F₆(),F₄()) = ((F₅(),F₆()) >=0_goto ((card F₄()) + 2)) ';' (F₄() ';' (goto (- ((card F₄()) + 1)))) by SCMPDS_4:15;
set Q2 = Q +* (stop F₄());
set Q3 = Q +* (stop (while<0 (F₅(),F₆(),F₄())));
set t4 = Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,1);
set Q4 = Q +* (stop (while<0 (F₅(),F₆(),F₄())));
A20: stop F₄() c= Q +* (stop F₄()) by FUNCT_4:25;
set m2 = LifeSpan ((Q +* (stop F₄())),t);
set t5 = Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,1)),(LifeSpan ((Q +* (stop F₄())),t)));
set Q5 = Q +* (stop (while<0 (F₅(),F₆(),F₄())));
set l1 = (card F₄()) + 1;
A21: IC t = 0 by MEMSTR_0:def 8;
set m3 = (LifeSpan ((Q +* (stop F₄())),t)) + 1;
set t6 = Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,((LifeSpan ((Q +* (stop F₄())),t)) + 1));
set Q6 = Q +* (stop (while<0 (F₅(),F₆(),F₄())));
set t7 = Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1));
set Q7 = Q +* (stop (while<0 (F₅(),F₆(),F₄())));
(card F₄()) + 1 < (card F₄()) + 2 by XREAL_1:6;
then A22: (card F₄()) + 1 in dom (while<0 (F₅(),F₆(),F₄())) by Th7;
AA: stop (while<0 (F₅(),F₆(),F₄())) c= Q +* (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 A23: while<0 (F₅(),F₆(),F₄()) c= Q +* (stop (while<0 (F₅(),F₆(),F₄()))) by AA, XBOOLE_1:1;
Shift (F₄(),1) c= while<0 (F₅(),F₆(),F₄()) by Lm2;
then A24: Shift (F₄(),1) c= Q +* (stop (while<0 (F₅(),F₆(),F₄()))) by A23, XBOOLE_1:1;
A25: Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(0 + 1)) = Following ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,0))) by EXTPRO_1:3
.= Following ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t) by EXTPRO_1:2
.= Exec (((F₅(),F₆()) >=0_goto ((card F₄()) + 2)),t) by A17, SCMPDS_6:11, T ;
for a being Int_position holds t . a = (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,1)) . a by A25, SCMPDS_2:57;
then A27: DataPart t = DataPart (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,1)) by SCMPDS_4:8;
F₄() is_halting_on t,Q by A4, A8, A9, A10;
then A28: Q +* (stop F₄()) halts_on t by SCMPDS_6:def 3, T;
(Q +* (stop F₄())) +* (stop F₄()) halts_on t by A28, FUNCT_4:25, FUNCT_4:98;
then A30: F₄() is_halting_on t,Q +* (stop F₄()) by SCMPDS_6:def 3, T;
A31: IExec (F₄(),Q,t) = Result ((Q +* (stop F₄())),t) by SCMPDS_4:def 5;
A32: P₁[ Initialize (IExec (F₄(),Q,t))] by A4, A8, A9, A10;
A33: F₄() is_closed_on t,Q by A4, A8, A9, A10;
A34: F₄() is_closed_on t,Q +* (stop F₄()) by A4, A8, A9, A10;
A35: IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,1)) = succ (IC t) by A10, A25, SCMPDS_2:57, A9
.= 0 + 1 by A21 ;
then A36: IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,1)),(LifeSpan ((Q +* (stop F₄())),t)))) = (card F₄()) + 1 by A20, A30, A34, A27, A24, SCMPDS_7:18;
A37: (Q +* (stop (while<0 (F₅(),F₆(),F₄())))) /. (IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,((LifeSpan ((Q +* (stop F₄())),t)) + 1)))) = (Q +* (stop (while<0 (F₅(),F₆(),F₄())))) . (IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,((LifeSpan ((Q +* (stop F₄())),t)) + 1)))) by PBOOLE:143;
A38: Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,((LifeSpan ((Q +* (stop F₄())),t)) + 1)) = Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,1)),(LifeSpan ((Q +* (stop F₄())),t))) by EXTPRO_1:4;
then A39: CurInstr ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,((LifeSpan ((Q +* (stop F₄())),t)) + 1)))) = (Q +* (stop (while<0 (F₅(),F₆(),F₄())))) . ((card F₄()) + 1) by A20, A30, A34, A35, A27, A24, A37, SCMPDS_7:18
.= (while<0 (F₅(),F₆(),F₄())) . ((card F₄()) + 1) by A22, A23, GRFUNC_1:2
.= goto (- ((card F₄()) + 1)) by Th8 ;
A41: Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1)) = Following ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,((LifeSpan ((Q +* (stop F₄())),t)) + 1)))) by EXTPRO_1:3
.= Exec ((goto (- ((card F₄()) + 1))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,((LifeSpan ((Q +* (stop F₄())),t)) + 1)))) by A39 ;
then IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1))) = ICplusConst ((Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,((LifeSpan ((Q +* (stop F₄())),t)) + 1))),(0 - ((card F₄()) + 1))) by SCMPDS_2:54
.= 0 by A36, A38, SCMPDS_7:1 ;
then A42: Initialize (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1))) = Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1)) by MEMSTR_0:46;
A43: DataPart (Comput ((Q +* (stop F₄())),t,(LifeSpan ((Q +* (stop F₄())),t)))) = DataPart (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,1)),(LifeSpan ((Q +* (stop F₄())),t)))) by A20, A30, A34, A35, A27, A24, SCMPDS_7:18;
then A44: DataPart (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,1)),(LifeSpan ((Q +* (stop F₄())),t)))) = DataPart (Result ((Q +* (stop F₄())),t)) by A28, EXTPRO_1:23
.= DataPart (IExec (F₄(),Q,t)) by SCMPDS_4:def 5 ;
InsCode (goto (- ((card F₄()) + 1))) = 0 by SCMPDS_2:12;
then InsCode (goto (- ((card F₄()) + 1))) in {0,4,5,6} by ENUMSET1:def 2;
then A45: Initialize (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1))) = Initialize (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,((LifeSpan ((Q +* (stop F₄())),t)) + 1))) by A41, Th3
.= Initialize (IExec (F₄(),Q,t)) by A44, A38, MEMSTR_0:80 ;

A46: now

F₁((Initialize (IExec (F₄(),Q,t)))) < F₁(t) by A4, A8, A9, A10;
then A47: F₁((Initialize (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1))))) < k + 1 by A7, A45, XXREAL_0:2;
assume F₁((Initialize (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1))))) > k ; :: thesis: contradiction
hence contradiction by A47, INT_1:7; :: thesis: verum

end;

A48: (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,1)),(LifeSpan ((Q +* (stop F₄())),t)))) . F₅() = (Comput ((Q +* (stop F₄())),t,(LifeSpan ((Q +* (stop F₄())),t)))) . F₅() by A43, SCMPDS_4:8
.= (Result ((Q +* (stop F₄())),t)) . F₅() by A28, EXTPRO_1:23
.= F₂() . F₅() by A9, A4, A8, A10, A31 ;
A50: (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1))) . F₅() = (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,((LifeSpan ((Q +* (stop F₄())),t)) + 1))) . F₅() by A41, SCMPDS_2:54
.= F₂() . F₅() by A48, EXTPRO_1:4 ;
then A51: while<0 (F₅(),F₆(),F₄()) is_closed_on Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1)),Q +* (stop (while<0 (F₅(),F₆(),F₄()))) by A6, A32, A45, A46, A42;

now

let k be Element of NAT ; :: thesis: IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,b₁)) in dom (stop (while<0 (F₅(),F₆(),F₄())))

per cases ( k < ((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1 or k >= ((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1 ) ;

suppose k < ((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1 ; :: thesis: IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,b₁)) in dom (stop (while<0 (F₅(),F₆(),F₄())))

then A52: k <= (LifeSpan ((Q +* (stop F₄())),t)) + 1 by INT_1:7;

hereby :: thesis: verum

per cases ( k <= LifeSpan ((Q +* (stop F₄())),t) or k = (LifeSpan ((Q +* (stop F₄())),t)) + 1 ) by A52, NAT_1:8;

suppose A53: k <= LifeSpan ((Q +* (stop F₄())),t) ; :: thesis: IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,k)) in dom (stop (while<0 (F₅(),F₆(),F₄())))

hereby :: thesis: verum

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,k)) in dom (stop (while<0 (F₅(),F₆(),F₄())))

hence IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,k)) in dom (stop (while<0 (F₅(),F₆(),F₄()))) by A14, A21, EXTPRO_1:2; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,k)) in dom (stop (while<0 (F₅(),F₆(),F₄())))

then consider kn being Nat such that
A54: k = kn + 1 by NAT_1:6;
reconsider kn = kn as Element of NAT by ORDINAL1:def 12;
reconsider lm = IC (Comput ((Q +* (stop F₄())),t,kn)) as Element of NAT ;
kn < k by A54, XREAL_1:29;
then kn < LifeSpan ((Q +* (stop F₄())),t) by A53, XXREAL_0:2;
then (IC (Comput ((Q +* (stop F₄())),t,kn))) + 1 = IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,1)),kn)) by A20, A30, A34, A35, A27, A24, SCMPDS_7:16;
then A56: IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,k)) = lm + 1 by A54, EXTPRO_1:4;
IC (Comput ((Q +* (stop F₄())),t,kn)) in dom (stop F₄()) by A33, SCMPDS_6:def 2, T;
then lm < card (stop F₄()) by AFINSQ_1:66;
then lm < (card F₄()) + 1 by COMPOS_1:55;
then A57: lm + 1 <= (card F₄()) + 1 by INT_1:7;
(card F₄()) + 1 < (card F₄()) + 3 by XREAL_1:6;
then lm + 1 < (card F₄()) + 3 by A57, XXREAL_0:2;
then lm + 1 < card (stop (while<0 (F₅(),F₆(),F₄()))) by Lm1;
hence IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,k)) in dom (stop (while<0 (F₅(),F₆(),F₄()))) by A56, AFINSQ_1:66; :: thesis: verum

end;

end;

end;

end;

suppose A58: k = (LifeSpan ((Q +* (stop F₄())),t)) + 1 ; :: thesis: IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,k)) in dom (stop (while<0 (F₅(),F₆(),F₄())))

(card F₄()) + 1 in dom (stop (while<0 (F₅(),F₆(),F₄()))) by A22, COMPOS_1:62;
hence IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,k)) in dom (stop (while<0 (F₅(),F₆(),F₄()))) by A20, A30, A34, A35, A27, A24, A38, A58, SCMPDS_7:18; :: thesis: verum

end;

end;

end;

end;

suppose k >= ((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1 ; :: thesis: IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,b₁)) in dom (stop (while<0 (F₅(),F₆(),F₄())))

then consider nn being Nat such that
A59: k = (((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1) + nn by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 12;
Q +* (stop (while<0 (F₅(),F₆(),F₄()))) = (Q +* (stop (while<0 (F₅(),F₆(),F₄())))) +* (stop (while<0 (F₅(),F₆(),F₄()))) by FUNCT_4:93;
then Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,k) = Comput (((Q +* (stop (while<0 (F₅(),F₆(),F₄())))) +* (stop (while<0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1))),nn) by A59, EXTPRO_1:4;
hence IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,k)) in dom (stop (while<0 (F₅(),F₆(),F₄()))) by A51, SCMPDS_6:def 2, A42; :: thesis: verum

end;

end;

end;

hence while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q by SCMPDS_6:def 2, T; :: thesis: while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q
RR: Q +* (stop (while<0 (F₅(),F₆(),F₄()))) = (Q +* (stop (while<0 (F₅(),F₆(),F₄())))) +* (stop (while<0 (F₅(),F₆(),F₄()))) by FUNCT_4:93;
while<0 (F₅(),F₆(),F₄()) is_halting_on Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1)),Q +* (stop (while<0 (F₅(),F₆(),F₄()))) by A6, A32, A50, A45, A46, A42;
then Q +* (stop (while<0 (F₅(),F₆(),F₄()))) halts_on Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),t,(((LifeSpan ((Q +* (stop F₄())),t)) + 1) + 1)) by A42, RR, SCMPDS_6:def 3;
then Q +* (stop (while<0 (F₅(),F₆(),F₄()))) halts_on t by EXTPRO_1:22;
hence while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q by SCMPDS_6:def 3, T; :: thesis: verum

end;

end;

end;

set n = F₁(F₂());
A60: S₁[ 0 ]

proof

let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st F₁(t) <= 0 & P₁[t] & t . F₅() = F₂() . F₅() holds
( while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q )
let Q be Instruction-Sequence of SCMPDS; :: thesis: ( F₁(t) <= 0 & P₁[t] & t . F₅() = F₂() . F₅() implies ( while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q ) )
assume that
A61: F₁(t) <= 0 and
A62: P₁[t] and
A63: t . F₅() = F₂() . F₅() ; :: thesis: ( while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q )
F₁(t) = 0 by A61;
then t . (DataLoc ((F₂() . F₅()),F₆())) >= 0 by A2, A62;
hence ( while<0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<0 (F₅(),F₆(),F₄()) is_halting_on t,Q ) by A63, Th9; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A60, A5);
then S₁[F₁(F₂())] ;
hence ( while<0 (F₅(),F₆(),F₄()) is_closed_on F₂(),F₃() & while<0 (F₅(),F₆(),F₄()) is_halting_on F₂(),F₃() ) by A3; :: thesis: verum