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 State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st F₁((Dstate t)) <= $1 & P₁[ Dstate 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]

now

let t be State of SCMPDS; :: thesis: for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st F₁((Dstate t)) <= k + 1 & P₁[ Dstate 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 the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: ( F₁((Dstate t)) <= k + 1 & P₁[ Dstate 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 A7: F₁((Dstate t)) <= k + 1 ; :: thesis: ( P₁[ Dstate 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 A8: P₁[ Dstate 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 A9: 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 A9, Th9; :: thesis: verum

end;

suppose A10: 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₂ )

A11: dom (ProgramPart t) = NAT by COMPOS_1:34;
A12: not F₅() in dom (t | NAT) by A11, SCMPDS_2:53;
A13: (IExec (F₄(),Q,t)) . F₅() = t . F₅() by A4, A8, A9, A10;
A14: 0 in dom (stop (while<0 (F₅(),F₆(),F₄()))) by COMPOS_1:135;
A15: dom (ProgramPart t) = NAT by COMPOS_1:34;
A16: not DataLoc ((F₂() . F₅()),F₆()) in dom (Start-At (0,SCMPDS)) by SCMPDS_4:59;
A17: while<0 (F₅(),F₆(),F₄()) = ((F₅(),F₆()) >=0_goto ((card F₄()) + 2)) ';' (F₄() ';' (goto (- ((card F₄()) + 1)))) by SCMPDS_4:51;
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₄())));
A20: stop F₄() c= Q +* (stop F₄()) by FUNCT_4:26;
B20: Start-At (0,SCMPDS) c= Initialize t by FUNCT_4:26;
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 l1 = (card F₄()) + 1;
A21: IC (Initialize t) = 0 by COMPOS_1:def 16;
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₄()) + 1 < (card F₄()) + 2 by XREAL_1:8;
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:26;
while<0 (F₅(),F₆(),F₄()) c= stop (while<0 (F₅(),F₆(),F₄())) by AFINSQ_1:78;
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 Shift (F₄(),1) c= Q +* (stop (while<0 (F₅(),F₆(),F₄()))) by A23, XBOOLE_1:1;
then A24: Shift (F₄(),1) c= Q +* (stop (while<0 (F₅(),F₆(),F₄()))) ;
A25: 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:4
.= Following ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Initialize t)) by EXTPRO_1:3
.= Exec (((F₅(),F₆()) >=0_goto ((card F₄()) + 2)),(Initialize t)) by A17, SCMPDS_6:22 ;

now

let a be Int_position ; :: thesis: (Initialize t) . a = (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Initialize t),1)) . a
thus (Initialize t) . a = (Initialize t) . a
.= (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Initialize t),1)) . a by A25, SCMPDS_2:69 ; :: thesis: verum

end;

then A27: DataPart (Initialize t) = DataPart (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Initialize t),1)) by SCMPDS_4:23;
F₄() is_halting_on t,Q by A4, A8, A9, A10;
then A28: Q +* (stop F₄()) halts_on Initialize t by SCMPDS_6:def 3;
Q +* (stop F₄()) = (Q +* (stop F₄())) +* (stop F₄()) by A20, FUNCT_4:104;
then (Q +* (stop F₄())) +* (stop F₄()) halts_on Initialize (Initialize t) by A28;
then A30: F₄() is_halting_on Initialize t,Q +* (stop F₄()) by SCMPDS_6:def 3;
A31: IExec (F₄(),Q,t) = (Result ((Q +* (stop F₄())),(Initialize t))) +* (t | NAT) by SCMPDS_4:def 8;
A32: P₁[ Dstate (IExec (F₄(),Q,t))] by A4, A8, A9, A10;
A33: F₄() is_closed_on t,Q by A4, A8, A9, A10;
then A34: F₄() is_closed_on Initialize t,Q +* (stop F₄()) by SCMPDS_6:38;
not F₅() in dom (Start-At (0,SCMPDS)) by SCMPDS_4:59;
then (Initialize t) . (DataLoc (((Initialize t) . F₅()),F₆())) = (Initialize t) . (DataLoc ((F₂() . F₅()),F₆())) by A9, FUNCT_4:12
.= t . (DataLoc ((F₂() . F₅()),F₆())) by A16, FUNCT_4:12 ;
then A35: IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Initialize t),1)) = succ (IC (Initialize t)) by A10, A25, SCMPDS_2:69
.= 0 + 1 by A21 ;
then A36: 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₄()) + 1 by A20, B20, A30, A34, A27, A24, SCMPDS_7:36;
A37: (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:158;
A38: 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:5;
then A39: 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₄()) + 1) by A20, B20, A30, A34, A35, A27, A24, A37, SCMPDS_7:36
.= (Q +* (stop (while<0 (F₅(),F₆(),F₄())))) . ((card F₄()) + 1)
.= (Q +* (stop (while<0 (F₅(),F₆(),F₄())))) . ((card F₄()) + 1)
.= (while<0 (F₅(),F₆(),F₄())) . ((card F₄()) + 1) by A22, A23, GRFUNC_1:8
.= goto (- ((card F₄()) + 1)) by Th8 ;
A41: 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:4
.= Exec ((goto (- ((card F₄()) + 1))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Initialize t),((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1)))) by A39 ;
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₄()) + 1))) by SCMPDS_2:66
.= 0 by A36, A38, SCMPDS_7:1 ;
then A42: 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 COMPOS_1:84;
A43: 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 A20, B20, A30, A34, A35, A27, A24, SCMPDS_7:36;
then A44: 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 A28, EXTPRO_1:23
.= DataPart ((Result ((Q +* (stop F₄())),(Initialize t))) +* (t | NAT)) by A15, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.= DataPart (IExec (F₄(),Q,t)) by SCMPDS_4:def 8 ;
InsCode (goto (- ((card F₄()) + 1))) = 0 by SCMPDS_2:21;
then InsCode (goto (- ((card F₄()) + 1))) in {0,4,5,6} by ENUMSET1:def 2;
then A45: Dstate (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Initialize t),(((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1))) = Dstate (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Initialize t),((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1))) by A41, Th3
.= Dstate (IExec (F₄(),Q,t)) by A44, A38, Th2 ;

A46: now

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

end;

A48: (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 A43, SCMPDS_4:23
.= (Result ((Q +* (stop F₄())),(Initialize t))) . F₅() by A28, EXTPRO_1:23
.= F₂() . F₅() by A9, A13, A31, A12, FUNCT_4:12 ;
A50: (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 A41, SCMPDS_2:66
.= F₂() . F₅() by A48, EXTPRO_1:5 ;
then A51: 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 A6, A32, A45, A46;

now

let k be Element of 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 A52: k <= (LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1 by INT_1:20;

hereby :: thesis: verum

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

suppose A53: 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 A14, A21, EXTPRO_1:3; :: 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
A54: k = kn + 1 by NAT_1:6;
reconsider kn = kn as Element of NAT by ORDINAL1:def 13;
reconsider lm = IC (Comput ((Q +* (stop F₄())),(Initialize t),kn)) as Element of NAT ;
kn < k by A54, XREAL_1:31;
then kn < LifeSpan ((Q +* (stop F₄())),(Initialize t)) by A53, XXREAL_0:2;
then (IC (Comput ((Q +* (stop F₄())),(Initialize t),kn))) + 1 = IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Initialize t),1)),kn)) by A20, B20, A30, A34, A35, A27, A24, SCMPDS_7:34;
then A56: IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Initialize t),k)) = lm + 1 by A54, EXTPRO_1:5;
IC (Comput ((Q +* (stop F₄())),(Initialize t),kn)) in dom (stop F₄()) by A33, SCMPDS_6:def 2;
then lm < card (stop F₄()) by AFINSQ_1:70;
then lm < (card F₄()) + 1 by SCMPDS_5:7;
then A57: lm + 1 <= (card F₄()) + 1 by INT_1:20;
(card F₄()) + 1 < (card F₄()) + 3 by XREAL_1:8;
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₄())))),(Initialize t),k)) in dom (stop (while<0 (F₅(),F₆(),F₄()))) by A56, AFINSQ_1:70; :: thesis: verum

end;

end;

end;

end;

suppose A58: 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₄()) + 1 in dom (stop (while<0 (F₅(),F₆(),F₄()))) by A22, SCMPDS_6:18;
hence IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Initialize t),k)) in dom (stop (while<0 (F₅(),F₆(),F₄()))) by A20, B20, A30, A34, A35, A27, A24, A38, A58, SCMPDS_7:36; :: 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
A59: k = (((LifeSpan ((Q +* (stop F₄())),(Initialize t))) + 1) + 1) + nn by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 13;
Q +* (stop (while<0 (F₅(),F₆(),F₄()))) = (Q +* (stop (while<0 (F₅(),F₆(),F₄())))) +* (stop (while<0 (F₅(),F₆(),F₄()))) by FUNCT_4:99;
then 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 A42, A59, EXTPRO_1:5;
hence IC (Comput ((Q +* (stop (while<0 (F₅(),F₆(),F₄())))),(Initialize t),k)) in dom (stop (while<0 (F₅(),F₆(),F₄()))) by A51, 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
RR: Q +* (stop (while<0 (F₅(),F₆(),F₄()))) = (Q +* (stop (while<0 (F₅(),F₆(),F₄())))) +* (stop (while<0 (F₅(),F₆(),F₄()))) by FUNCT_4:99;
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 A6, A32, A50, A45, A46;
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 A42, SCMPDS_6:def 3, RR;
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₁((Dstate F₂()));
thus ( F₁(F₂()) = F₁(F₂()) or P₁[F₂()] ) ; :: thesis: ( while<0 (F₅(),F₆(),F₄()) is_closed_on F₂(),F₃() & while<0 (F₅(),F₆(),F₄()) is_halting_on F₂(),F₃() )
A60: S₁[ 0 ]

proof

let t be State of SCMPDS; :: thesis: for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st F₁((Dstate t)) <= 0 & P₁[ Dstate 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 the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: ( F₁((Dstate t)) <= 0 & P₁[ Dstate 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₁((Dstate t)) <= 0 and
A62: P₁[ Dstate 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₁((Dstate 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₁((Dstate 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