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 iWHL = Initialized (stop (while>0 F₄(),F₅(),F₃()));
set pI = stop F₃();
set IsI = Initialized (stop F₃());
set b = DataLoc (F₂() . F₄()),F₅();
defpred S₁[ Element of NAT ] means for t being State of SCMPDS st F₁((Dstate t)) <= $1 & P₁[ Dstate t] & t . F₄() = F₂() . F₄() holds
( while>0 F₄(),F₅(),F₃() is_closed_on t & while>0 F₄(),F₅(),F₃() is_halting_on t );
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: ( F₁((Dstate t)) <= k + 1 & P₁[ Dstate t] & t . F₄() = F₂() . F₄() implies ( while>0 F₄(),F₅(),F₃() is_closed_on b₁ & while>0 F₄(),F₅(),F₃() is_halting_on 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₁ & while>0 F₄(),F₅(),F₃() is_halting_on b₁ ) )
assume A8: P₁[ Dstate t] ; :: thesis: ( t . F₄() = F₂() . F₄() implies ( while>0 F₄(),F₅(),F₃() is_closed_on b₁ & while>0 F₄(),F₅(),F₃() is_halting_on b₁ ) )
assume A9: t . F₄() = F₂() . F₄() ; :: thesis: ( while>0 F₄(),F₅(),F₃() is_closed_on b₁ & while>0 F₄(),F₅(),F₃() is_halting_on 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₁ & while>0 F₄(),F₅(),F₃() is_halting_on b₁ )

hence ( while>0 F₄(),F₅(),F₃() is_closed_on t & while>0 F₄(),F₅(),F₃() is_halting_on t ) by A9, Th20; :: thesis: verum

end;

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

A11: dom (t | NAT ) = NAT by SCMPDS_6:1;

A12: now

assume F₄() in dom (t | NAT ) ; :: thesis: contradiction
then reconsider l = F₄() as Instruction-Location of SCMPDS by A11, AMI_1:def 4;
l = F₄() ;
hence contradiction by SCMPDS_2:53; :: thesis: verum

end;

A13: (IExec F₃(),t) . F₄() = t . F₄() by A4, A8, A9, A10;
A14: inspos 0 in dom (stop (while>0 F₄(),F₅(),F₃())) by SCMPDS_4:75;
A15: dom (t | NAT ) = NAT by SCMPDS_6:1;
A16: not DataLoc (F₂() . F₄()),F₅() in dom (Initialized (stop (while>0 F₄(),F₅(),F₃()))) by SCMPDS_4:31;
A17: while>0 F₄(),F₅(),F₃() = (F₄(),F₅() <=0_goto ((card F₃()) + 2)) ';' (F₃() ';' (goto (- ((card F₃()) + 1)))) by SCMPDS_4:51;
set t2 = t +* (Initialized (stop F₃()));
set t3 = t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())));
set t4 = Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1;
A18: Initialized (stop F₃()) c= t +* (Initialized (stop F₃())) by FUNCT_4:26;
set m2 = LifeSpan (t +* (Initialized (stop F₃())));
set t5 = Computation (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1),(LifeSpan (t +* (Initialized (stop F₃()))));
set l1 = inspos ((card F₃()) + 1);
A19: IC (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))) = inspos 0 by SCMPDS_6:21;
set m3 = (LifeSpan (t +* (Initialized (stop F₃())))) + 1;
set t6 = Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),((LifeSpan (t +* (Initialized (stop F₃())))) + 1);
set t7 = Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1);
(card F₃()) + 1 < (card F₃()) + 2 by XREAL_1:8;
then A20: inspos ((card F₃()) + 1) in dom (while>0 F₄(),F₅(),F₃()) by Th18;
( while>0 F₄(),F₅(),F₃() c= Initialized (stop (while>0 F₄(),F₅(),F₃())) & Initialized (stop (while>0 F₄(),F₅(),F₃())) c= t +* (Initialized (stop (while>0 F₄(),F₅(),F₃()))) ) by FUNCT_4:26, SCMPDS_6:17;
then A21: while>0 F₄(),F₅(),F₃() c= t +* (Initialized (stop (while>0 F₄(),F₅(),F₃()))) by XBOOLE_1:1;
Shift F₃(),1 c= while>0 F₄(),F₅(),F₃() by Lm4;
then Shift F₃(),1 c= t +* (Initialized (stop (while>0 F₄(),F₅(),F₃()))) by A21, XBOOLE_1:1;
then A22: Shift F₃(),1 c= Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1 by AMI_1:81;
A23: Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(0 + 1) = Following (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),0 ) by AMI_1:14
.= Following (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))) by AMI_1:13
.= Exec (F₄(),F₅() <=0_goto ((card F₃()) + 2)),(t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))) by A17, SCMPDS_6:22 ;
A24: DataPart (t +* (Initialized (stop F₃()))) = DataPart (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))) by SCMPDS_4:24, SCMPDS_4:36;

now

let a be Int_position ; :: thesis: (t +* (Initialized (stop F₃()))) . a = (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1) . a
thus (t +* (Initialized (stop F₃()))) . a = (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))) . a by A24, SCMPDS_4:23
.= (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1) . a by A23, SCMPDS_2:68 ; :: thesis: verum

end;

then A25: DataPart (t +* (Initialized (stop F₃()))) = DataPart (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1) by SCMPDS_4:23;
F₃() is_halting_on t by A4, A8, A9, A10;
then A26: t +* (Initialized (stop F₃())) is halting by SCMPDS_6:def 3;
then (t +* (Initialized (stop F₃()))) +* (Initialized (stop F₃())) is halting by A18, FUNCT_4:79;
then A27: F₃() is_halting_on t +* (Initialized (stop F₃())) by SCMPDS_6:def 3;
A28: IExec F₃(),t = (Result (t +* (Initialized (stop F₃())))) +* (t | NAT ) by SCMPDS_4:def 8;
A29: P₁[ Dstate (IExec F₃(),t)] by A4, A8, A9, A10;
A30: F₃() is_closed_on t by A4, A8, A9, A10;
then A31: F₃() is_closed_on t +* (Initialized (stop F₃())) by SCMPDS_6:38;
not F₄() in dom (Initialized (stop (while>0 F₄(),F₅(),F₃()))) by SCMPDS_4:31;
then (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))) . (DataLoc ((t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))) . F₄()),F₅()) = (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))) . (DataLoc (F₂() . F₄()),F₅()) by A9, FUNCT_4:12
.= t . (DataLoc (F₂() . F₄()),F₅()) by A16, FUNCT_4:12 ;
then A32: IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1) = Next (IC (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃()))))) by A10, A23, SCMPDS_2:68
.= inspos (0 + 1) by A19 ;
then A33: IC (Computation (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1),(LifeSpan (t +* (Initialized (stop F₃()))))) = inspos ((card F₃()) + 1) by A1, A18, A27, A31, A25, A22, SCMPDS_7:36;
A34: Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),((LifeSpan (t +* (Initialized (stop F₃())))) + 1) = Computation (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1),(LifeSpan (t +* (Initialized (stop F₃())))) by AMI_1:51;
then A35: CurInstr (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),((LifeSpan (t +* (Initialized (stop F₃())))) + 1)) = (Computation (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1),(LifeSpan (t +* (Initialized (stop F₃()))))) . (inspos ((card F₃()) + 1)) by A1, A18, A27, A31, A32, A25, A22, SCMPDS_7:36
.= (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1) . (inspos ((card F₃()) + 1)) by AMI_1:54
.= (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))) . (inspos ((card F₃()) + 1)) by AMI_1:54
.= (while>0 F₄(),F₅(),F₃()) . (inspos ((card F₃()) + 1)) by A20, A21, GRFUNC_1:8
.= goto (- ((card F₃()) + 1)) by Th19 ;
A36: Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1) = Following (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),((LifeSpan (t +* (Initialized (stop F₃())))) + 1)) by AMI_1:14
.= Exec (goto (- ((card F₃()) + 1))),(Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),((LifeSpan (t +* (Initialized (stop F₃())))) + 1)) by A35 ;
then IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1)) = ICplusConst (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),((LifeSpan (t +* (Initialized (stop F₃())))) + 1)),(0 - ((card F₃()) + 1)) by SCMPDS_2:66
.= inspos 0 by A33, A34, SCMPDS_7:1 ;
then A37: (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1)) +* (Initialized (stop (while>0 F₄(),F₅(),F₃()))) = Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1) by SCMPDS_7:37;
A38: DataPart (Computation (t +* (Initialized (stop F₃()))),(LifeSpan (t +* (Initialized (stop F₃()))))) = DataPart (Computation (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1),(LifeSpan (t +* (Initialized (stop F₃()))))) by A1, A18, A27, A31, A32, A25, A22, SCMPDS_7:36;
then A39: DataPart (Computation (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1),(LifeSpan (t +* (Initialized (stop F₃()))))) = DataPart (Result (t +* (Initialized (stop F₃())))) by A26, AMI_1:122
.= DataPart ((Result (t +* (Initialized (stop F₃())))) +* (t | NAT )) by A15, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.= DataPart (IExec F₃(),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 A40: Dstate (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1)) = Dstate (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),((LifeSpan (t +* (Initialized (stop F₃())))) + 1)) by A36, Th3
.= Dstate (IExec F₃(),t) by A39, A34, Th2 ;

A41: now

F₁((Dstate (IExec F₃(),t))) < F₁((Dstate t)) by A4, A8, A9, A10;
then A42: F₁((Dstate (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1)))) < k + 1 by A7, A40, XXREAL_0:2;
assume F₁((Dstate (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1)))) > k ; :: thesis: contradiction
hence contradiction by A42, INT_1:20; :: thesis: verum

end;

A43: (Computation (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1),(LifeSpan (t +* (Initialized (stop F₃()))))) . F₄() = (Computation (t +* (Initialized (stop F₃()))),(LifeSpan (t +* (Initialized (stop F₃()))))) . F₄() by A38, SCMPDS_4:23
.= (Result (t +* (Initialized (stop F₃())))) . F₄() by A26, AMI_1:122
.= F₂() . F₄() by A9, A13, A28, A12, FUNCT_4:12 ;
A44: (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1)) . F₄() = (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),((LifeSpan (t +* (Initialized (stop F₃())))) + 1)) . F₄() by A36, SCMPDS_2:66
.= F₂() . F₄() by A43, AMI_1:51 ;
then A45: while>0 F₄(),F₅(),F₃() is_closed_on Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1) by A6, A29, A40, A41;

now

let k be Element of NAT ; :: thesis: IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),b₁) in dom (stop (while>0 F₄(),F₅(),F₃()))

per cases ( k < ((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1 or k >= ((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1 ) ;

suppose k < ((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1 ; :: thesis: IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),b₁) in dom (stop (while>0 F₄(),F₅(),F₃()))

then A46: k <= (LifeSpan (t +* (Initialized (stop F₃())))) + 1 by INT_1:20;

hereby :: thesis: verum

per cases ( k <= LifeSpan (t +* (Initialized (stop F₃()))) or k = (LifeSpan (t +* (Initialized (stop F₃())))) + 1 ) by A46, NAT_1:8;

suppose A47: k <= LifeSpan (t +* (Initialized (stop F₃()))) ; :: thesis: IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),k) in dom (stop (while>0 F₄(),F₅(),F₃()))

hereby :: thesis: verum

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

suppose k = 0 ; :: thesis: IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),k) in dom (stop (while>0 F₄(),F₅(),F₃()))

hence IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),k) in dom (stop (while>0 F₄(),F₅(),F₃())) by A14, A19, AMI_1:13; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),k) in dom (stop (while>0 F₄(),F₅(),F₃()))

then consider kn being Nat such that
A48: k = kn + 1 by NAT_1:6;
reconsider kn = kn as Element of NAT by ORDINAL1:def 13;
reconsider lm = IC (Computation (t +* (Initialized (stop F₃()))),kn) as Element of NAT by ORDINAL1:def 13;
kn < k by A48, XREAL_1:31;
then kn < LifeSpan (t +* (Initialized (stop F₃()))) by A47, XXREAL_0:2;
then (IC (Computation (t +* (Initialized (stop F₃()))),kn)) + 1 = IC (Computation (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),1),kn) by A1, A18, A27, A31, A32, A25, A22, SCMPDS_7:34;
then A49: IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),k) = inspos (lm + 1) by A48, AMI_1:51;
IC (Computation (t +* (Initialized (stop F₃()))),kn) in dom (stop F₃()) by A30, SCMPDS_6:def 2;
then lm < card (stop F₃()) by SCMPDS_4:1;
then lm < (card F₃()) + 1 by SCMPDS_5:7;
then A50: 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 A50, XXREAL_0:2;
then lm + 1 < card (stop (while>0 F₄(),F₅(),F₃())) by Lm3;
hence IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),k) in dom (stop (while>0 F₄(),F₅(),F₃())) by A49, SCMPDS_4:1; :: thesis: verum

end;

end;

end;

end;

suppose A51: k = (LifeSpan (t +* (Initialized (stop F₃())))) + 1 ; :: thesis: IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),k) in dom (stop (while>0 F₄(),F₅(),F₃()))

inspos ((card F₃()) + 1) in dom (stop (while>0 F₄(),F₅(),F₃())) by A20, SCMPDS_6:18;
hence IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),k) in dom (stop (while>0 F₄(),F₅(),F₃())) by A1, A18, A27, A31, A32, A25, A22, A34, A51, SCMPDS_7:36; :: thesis: verum

end;

end;

end;

end;

suppose k >= ((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1 ; :: thesis: IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),b₁) in dom (stop (while>0 F₄(),F₅(),F₃()))

then consider nn being Nat such that
A52: k = (((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1) + nn by NAT_1:10;
A53: nn in NAT by ORDINAL1:def 13;
then Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),k = Computation ((Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1)) +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),nn by A37, A52, AMI_1:51;
hence IC (Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),k) in dom (stop (while>0 F₄(),F₅(),F₃())) by A45, A53, SCMPDS_6:def 2; :: thesis: verum

end;

end;

end;

hence while>0 F₄(),F₅(),F₃() is_closed_on t by SCMPDS_6:def 2; :: thesis: while>0 F₄(),F₅(),F₃() is_halting_on t
while>0 F₄(),F₅(),F₃() is_halting_on Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1) by A6, A29, A44, A40, A41;
then Computation (t +* (Initialized (stop (while>0 F₄(),F₅(),F₃())))),(((LifeSpan (t +* (Initialized (stop F₃())))) + 1) + 1) is halting by A37, SCMPDS_6:def 3;
then t +* (Initialized (stop (while>0 F₄(),F₅(),F₃()))) is halting by AMI_1:93;
hence while>0 F₄(),F₅(),F₃() is_halting_on t 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₂() & while>0 F₄(),F₅(),F₃() is_halting_on F₂() )
A54: S₁[ 0 ]

proof

let t be State of SCMPDS ; :: thesis: ( F₁((Dstate t)) <= 0 & P₁[ Dstate t] & t . F₄() = F₂() . F₄() implies ( while>0 F₄(),F₅(),F₃() is_closed_on t & while>0 F₄(),F₅(),F₃() is_halting_on t ) )
assume that
A55: F₁((Dstate t)) <= 0 and
A56: P₁[ Dstate t] and
A57: t . F₄() = F₂() . F₄() ; :: thesis: ( while>0 F₄(),F₅(),F₃() is_closed_on t & while>0 F₄(),F₅(),F₃() is_halting_on t )
F₁((Dstate t)) = 0 by A55;
then t . (DataLoc (F₂() . F₄()),F₅()) <= 0 by A2, A56;
hence ( while>0 F₄(),F₅(),F₃() is_closed_on t & while>0 F₄(),F₅(),F₃() is_halting_on t ) by A57, Th20; :: thesis: verum

end;

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