A4: Initialize F₂() = F₂() by MEMSTR_0:44;
set i1 = (F₅(),F₆()) <>0_goto 2;
set i2 = goto ((card F₄()) + 2);
set i3 = goto (- ((card F₄()) + 2));
set WHL = while<>0 (F₅(),F₆(),F₄());
set pWH = stop (while<>0 (F₅(),F₆(),F₄()));
set pI = stop F₄();
set b = DataLoc ((F₂() . F₅()),F₆());
defpred S₁[ Nat] means for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st F₁((Initialize t)) <= $1 & P₁[ Initialize 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 Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st F₁((Initialize t)) <= k + 1 & P₁[ Initialize 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 t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st F₁((Initialize t)) <= k + 1 & P₁[ Initialize t] & t . F₅() = F₂() . F₅() holds
( while<>0 (F₅(),F₆(),F₄()) is_closed_on b₂,b₃ & while<>0 (F₅(),F₆(),F₄()) is_halting_on b₂,b₃ )
let Q be Instruction-Sequence of SCMPDS; :: thesis: ( F₁((Initialize t)) <= k + 1 & P₁[ Initialize t] & t . F₅() = F₂() . F₅() implies ( while<>0 (F₅(),F₆(),F₄()) is_closed_on b₁,b₂ & while<>0 (F₅(),F₆(),F₄()) is_halting_on b₁,b₂ ) )
A7: Initialize t = t by MEMSTR_0:44;
assume A8: F₁((Initialize t)) <= k + 1 ; :: thesis: ( P₁[ Initialize t] & t . F₅() = F₂() . F₅() implies ( while<>0 (F₅(),F₆(),F₄()) is_closed_on b₁,b₂ & while<>0 (F₅(),F₆(),F₄()) is_halting_on b₁,b₂ ) )
assume A9: P₁[ Initialize t] ; :: thesis: ( t . F₅() = F₂() . F₅() implies ( while<>0 (F₅(),F₆(),F₄()) is_closed_on b₁,b₂ & while<>0 (F₅(),F₆(),F₄()) is_halting_on b₁,b₂ ) )
assume A10: t . F₅() = F₂() . F₅() ; :: thesis: ( while<>0 (F₅(),F₆(),F₄()) is_closed_on b₁,b₂ & while<>0 (F₅(),F₆(),F₄()) is_halting_on b₁,b₂ )

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 b₁,b₂ & while<>0 (F₅(),F₆(),F₄()) is_halting_on b₁,b₂ )

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

end;

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

A12: (IExec (F₄(),Q,t)) . F₅() = t . F₅() by A3, A9, A10, A11, A7;
A13: 0 in dom (stop (while<>0 (F₅(),F₆(),F₄()))) by COMPOS_1:36;
A14: while<>0 (F₅(),F₆(),F₄()) = ((F₅(),F₆()) <>0_goto 2) ';' (((goto ((card F₄()) + 2)) ';' F₄()) ';' (goto (- ((card F₄()) + 2)))) by Lm8;
A15: not DataLoc ((F₂() . F₅()),F₆()) in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;
set t2 = Initialize t;
set Q2 = Q +* (stop F₄());
set t3 = Initialize t;
set Q3 = Q +* (stop (while<>0 (F₅(),F₆(),F₄())));
set t4 = Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),1);
set Q4 = Q +* (stop (while<>0 (F₅(),F₆(),F₄())));
A16: stop F₄() c= Q +* (stop F₄()) by FUNCT_4:25;
set m2 = LifeSpan ((Q +* (stop F₄())),(Initialize t));
set t5 = Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),1)),(LifeSpan ((Q +* (stop F₄())),(Initialize t))));
set Q5 = Q +* (stop (while<>0 (F₅(),F₆(),F₄())));
set l2 = (card F₄()) + 2;
A17: IC (Initialize t) = 0 by MEMSTR_0:47;
set m3 = (LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1;
set t6 = Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1));
set Q6 = Q +* (stop (while<>0 (F₅(),F₆(),F₄())));
set t7 = Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1));
set Q7 = Q +* (stop (while<>0 (F₅(),F₆(),F₄())));
(card F₄()) + 2 < (card F₄()) + 3 by XREAL_1:6;
then A18: (card F₄()) + 2 in dom (while<>0 (F₅(),F₆(),F₄())) by Th9;
A19: 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 A20: while<>0 (F₅(),F₆(),F₄()) c= Q +* (stop (while<>0 (F₅(),F₆(),F₄()))) by A19, XBOOLE_1:1;
Shift (F₄(),2) c= while<>0 (F₅(),F₆(),F₄()) by Lm9;
then Shift (F₄(),2) c= Q +* (stop (while<>0 (F₅(),F₆(),F₄()))) by A20, XBOOLE_1:1;
then A21: Shift (F₄(),2) c= Q +* (stop (while<>0 (F₅(),F₆(),F₄()))) ;
A22: Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(0 + 1)) = Following ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),0))) by EXTPRO_1:3
.= Following ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t))
.= Exec (((F₅(),F₆()) <>0_goto 2),(Initialize t)) by A14, SCMPDS_6:11 ;
for a being Int_position holds (Initialize t) . a = (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),1)) . a by A22, SCMPDS_2:55;
then A23: DataPart (Initialize t) = DataPart (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),1)) by SCMPDS_4:8;
F₄() is_halting_on t,Q by A3, A9, A10, A11, A7;
then A24: Q +* (stop F₄()) halts_on Initialize t by SCMPDS_6:def 3;
(Q +* (stop F₄())) +* (stop F₄()) halts_on Initialize (Initialize t) by A24;
then A25: F₄() is_halting_on Initialize t,Q +* (stop F₄()) by SCMPDS_6:def 3;
A26: IExec (F₄(),Q,(Initialize t)) = Result ((Q +* (stop F₄())),(Initialize t)) by SCMPDS_4:def 5;
A27: P₁[ Initialize (IExec (F₄(),Q,(Initialize t)))] by A3, A9, A10, A11, A7;
A28: F₄() is_closed_on t,Q by A3, A9, A10, A11, A7;
then A29: F₄() is_closed_on Initialize t,Q +* (stop F₄()) by SCMPDS_6:24;
not F₅() in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;
then (Initialize t) . (DataLoc (((Initialize t) . F₅()),F₆())) = (Initialize t) . (DataLoc ((F₂() . F₅()),F₆())) by A10, FUNCT_4:11
.= t . (DataLoc ((F₂() . F₅()),F₆())) by A15, FUNCT_4:11 ;
then A30: IC (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),1)) = ICplusConst ((Initialize t),2) by A11, A22, SCMPDS_2:55
.= 0 + 2 by A17, SCMPDS_6:12 ;
then A31: IC (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),1)),(LifeSpan ((Q +* (stop F₄())),(Initialize t))))) = (card F₄()) + 2 by A16, A25, A29, A23, A21, SCMPDS_7:18;
A32: (Q +* (stop (while<>0 (F₅(),F₆(),F₄())))) /. (IC (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1)))) = (Q +* (stop (while<>0 (F₅(),F₆(),F₄())))) . (IC (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1)))) by PBOOLE:143;
A33: Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1)) = Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),1)),(LifeSpan ((Q +* (stop F₄())),(Initialize t)))) by EXTPRO_1:4;
then A34: CurInstr ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1)))) = (Q +* (stop (while<>0 (F₅(),F₆(),F₄())))) . ((card F₄()) + 2) by A16, A25, A29, A30, A23, A21, A32, SCMPDS_7:18
.= (Q +* (stop (while<>0 (F₅(),F₆(),F₄())))) . ((card F₄()) + 2)
.= (Q +* (stop (while<>0 (F₅(),F₆(),F₄())))) . ((card F₄()) + 2)
.= (while<>0 (F₅(),F₆(),F₄())) . ((card F₄()) + 2) by A18, A20, GRFUNC_1:2
.= goto (- ((card F₄()) + 2)) by Th11 ;
A35: Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1)) = Following ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1)))) by EXTPRO_1:3
.= Exec ((goto (- ((card F₄()) + 2))),(Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1)))) by A34 ;
then IC (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1))) = ICplusConst ((Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1))),(0 - ((card F₄()) + 2))) by SCMPDS_2:54
.= 0 by A31, A33, SCMPDS_7:1 ;
then A36: Initialize (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1))) = Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1)) by MEMSTR_0:46;
A37: (Q +* (stop (while<>0 (F₅(),F₆(),F₄())))) +* (stop (while<>0 (F₅(),F₆(),F₄()))) = Q +* (stop (while<>0 (F₅(),F₆(),F₄()))) ;
A38: DataPart (Comput ((Q +* (stop F₄())),(Initialize t),(LifeSpan ((Q +* (stop F₄())),(Initialize t))))) = DataPart (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),1)),(LifeSpan ((Q +* (stop F₄())),(Initialize t))))) by A16, A25, A29, A30, A23, A21, SCMPDS_7:18;
then A39: DataPart (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),1)),(LifeSpan ((Q +* (stop F₄())),(Initialize t))))) = DataPart (Result ((Q +* (stop F₄())),(Initialize t))) by A24, EXTPRO_1:23
.= DataPart (Result ((Q +* (stop F₄())),(Initialize t)))
.= DataPart (IExec (F₄(),Q,(Initialize t))) by SCMPDS_4:def 5 ;
InsCode (goto (- ((card F₄()) + 2))) = 14 by SCMPDS_2:12;
then InsCode (goto (- ((card F₄()) + 2))) in {0,4,5,6,14} by ENUMSET1:def 3;
then A40: Initialize (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1))) = Initialize (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1))) by A35, SCMPDS_8:3
.= Initialize (IExec (F₄(),Q,(Initialize t))) by A39, A33, MEMSTR_0:80 ;

A41: now :: thesis: not F₁((Initialize (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1))))) > k

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

end;

A43: (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),1)),(LifeSpan ((Q +* (stop F₄())),(Initialize t))))) . F₅() = (Comput ((Q +* (stop F₄())),(Initialize t),(LifeSpan ((Q +* (stop F₄())),(Initialize t))))) . F₅() by A38, SCMPDS_4:8
.= (Result ((Q +* (stop F₄())),(Initialize t))) . F₅() by A24, EXTPRO_1:23
.= F₂() . F₅() by A10, A12, A26, A7 ;
A44: (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1))) . F₅() = (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1))) . F₅() by A35, SCMPDS_2:54
.= F₂() . F₅() by A43, EXTPRO_1:4 ;
A45: (Initialize (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1)))) . F₅() = (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1))) . F₅() by SCMPDS_5:15;
P₁[ Initialize (Initialize (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1))))] by A27, A40;
then A46: ( while<>0 (F₅(),F₆(),F₄()) is_closed_on Initialize (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1))),Q +* (stop (while<>0 (F₅(),F₆(),F₄()))) & while<>0 (F₅(),F₆(),F₄()) is_halting_on Initialize (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1))),Q +* (stop (while<>0 (F₅(),F₆(),F₄()))) ) by A6, A41, A44, A45;
A47: while<>0 (F₅(),F₆(),F₄()) is_closed_on Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1)),Q +* (stop (while<>0 (F₅(),F₆(),F₄())))

proof

for k being Nat holds IC (Comput (((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))) +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (Initialize (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1))))),k)) in dom (stop (while<>0 (F₅(),F₆(),F₄()))) by A46, SCMPDS_6:def 2;
hence while<>0 (F₅(),F₆(),F₄()) is_closed_on Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1)),Q +* (stop (while<>0 (F₅(),F₆(),F₄()))) by SCMPDS_6:def 2; :: thesis: verum

end;

now :: thesis: for k being Nat holds IC (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),k)) in dom (stop (while<>0 (F₅(),F₆(),F₄())))

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

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

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

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

hereby :: thesis: verum

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

suppose A49: k <= LifeSpan ((Q +* (stop F₄())),(Initialize t)) ; :: thesis: IC (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize 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₄())))),(Initialize t),k)) in dom (stop (while<>0 (F₅(),F₆(),F₄())))

hence IC (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),k)) in dom (stop (while<>0 (F₅(),F₆(),F₄()))) by A13, A17; :: thesis: verum

end;

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

then consider kn being Nat such that
A50: 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₄())),(Initialize t),kn)) as Element of NAT ;
kn < k by A50, XREAL_1:29;
then kn < LifeSpan ((Q +* (stop F₄())),(Initialize t)) by A49, XXREAL_0:2;
then (IC (Comput ((Q +* (stop F₄())),(Initialize t),kn))) + 2 = IC (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),1)),kn)) by A16, A25, A29, A30, A23, A21, SCMPDS_7:16;
then A51: IC (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),k)) = lm + 2 by A50, EXTPRO_1:4;
IC (Comput ((Q +* (stop F₄())),(Initialize t),kn)) in dom (stop F₄()) by A28, SCMPDS_6:def 2;
then lm < card (stop F₄()) by AFINSQ_1:66;
then lm < (card F₄()) + 1 by COMPOS_1:55;
then A52: lm + 2 < ((card F₄()) + 1) + 2 by XREAL_1:6;
(card F₄()) + 3 < (card F₄()) + 4 by XREAL_1:6;
then lm + 2 < (card F₄()) + 4 by A52, XXREAL_0:2;
then lm + 2 < card (stop (while<>0 (F₅(),F₆(),F₄()))) by Lm7;
hence IC (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),k)) in dom (stop (while<>0 (F₅(),F₆(),F₄()))) by A51, AFINSQ_1:66; :: thesis: verum

end;

end;

end;

end;

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

(card F₄()) + 2 in dom (stop (while<>0 (F₅(),F₆(),F₄()))) by A18, COMPOS_1:62;
hence IC (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),k)) in dom (stop (while<>0 (F₅(),F₆(),F₄()))) by A16, A25, A29, A30, A23, A21, A33, A53, SCMPDS_7:18; :: thesis: verum

end;

end;

end;

end;

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

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

end;

end;

end;

hence while<>0 (F₅(),F₆(),F₄()) is_closed_on t,Q by SCMPDS_6:def 2; :: thesis: while<>0 (F₅(),F₆(),F₄()) is_halting_on t,Q
while<>0 (F₅(),F₆(),F₄()) is_halting_on Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1)),Q +* (stop (while<>0 (F₅(),F₆(),F₄())))

proof

(Q +* (stop (while<>0 (F₅(),F₆(),F₄())))) +* (stop (while<>0 (F₅(),F₆(),F₄()))) halts_on Initialize (Initialize (Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1)))) by A46, SCMPDS_6:def 3;
hence while<>0 (F₅(),F₆(),F₄()) is_halting_on Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1)),Q +* (stop (while<>0 (F₅(),F₆(),F₄()))) by SCMPDS_6:def 3; :: thesis: verum

end;

then Q +* (stop (while<>0 (F₅(),F₆(),F₄()))) halts_on Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1)) by A37, A36, SCMPDS_6:def 3;
then Q +* (stop (while<>0 (F₅(),F₆(),F₄()))) halts_on Comput ((Q +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1)) ;
then Q +* (stop (while<>0 (F₅(),F₆(),F₄()))) halts_on Initialize t by EXTPRO_1:22;
hence while<>0 (F₅(),F₆(),F₄()) is_halting_on t,Q by SCMPDS_6:def 3; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

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

proof

let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st F₁((Initialize t)) <= 0 & P₁[ Initialize 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₁((Initialize t)) <= 0 & P₁[ Initialize 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
A56: ( F₁((Initialize t)) <= 0 & P₁[ Initialize t] ) and
A57: 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 )
(Initialize t) . (DataLoc ((F₂() . F₅()),F₆())) = t . (DataLoc ((F₂() . F₅()),F₆())) by SCMPDS_5:15;
then t . (DataLoc ((F₂() . F₅()),F₆())) = 0 by A1, A56, XXREAL_0:1;
hence ( while<>0 (F₅(),F₆(),F₄()) is_closed_on t,Q & while<>0 (F₅(),F₆(),F₄()) is_halting_on t,Q ) by A57, Th12; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A55, 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 A2, A4; :: thesis: verum