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 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 (ProgramPart t) = NAT by COMPOS_1:34;
A12: not F₄() in dom (t | NAT ) by A11, SCMPDS_2:53;
A13: (IExec F₃(),t) . F₄() = t . F₄() by A4, A8, A9, A10;
A14: 0 in dom (stop (while>0 F₄(),F₅(),F₃())) by SCMPDS_4:75;
A15: dom (ProgramPart t) = NAT by COMPOS_1:34;
A16: not DataLoc (F₂() . F₄()),F₅() in dom (Initialize (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;
I1: (Initialize t) +* (stop F₃()) = t +* (Initialize (stop F₃())) by SCMPDS_4:5;
I2: (Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())) = t +* (Initialize (stop (while>0 F₄(),F₅(),F₃()))) by SCMPDS_4:5;
set t2 = (Initialize t) +* (stop F₃());
set t3 = (Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()));
set t4 = Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1;
A18: Initialize (stop F₃()) c= (Initialize t) +* (stop F₃()) by I1, FUNCT_4:26;
set m2 = LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()));
set t5 = Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1),(LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃())));
set l1 = (card F₃()) + 1;
A19: IC ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) = 0 by SCMPDS_6:21;
set m3 = (LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1;
set t6 = Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1);
set t7 = Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1);
(card F₃()) + 1 < (card F₃()) + 2 by XREAL_1:8;
then A20: (card F₃()) + 1 in dom (while>0 F₄(),F₅(),F₃()) by Th18;
( while>0 F₄(),F₅(),F₃() c= Initialize (stop (while>0 F₄(),F₅(),F₃())) & Initialize (stop (while>0 F₄(),F₅(),F₃())) c= (Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())) ) by I2, FUNCT_4:26, SCMPDS_6:17;
then A21: while>0 F₄(),F₅(),F₃() c= (Initialize t) +* (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= (Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())) by A21, XBOOLE_1:1;
then A22: Shift F₃(),1 c= Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1 by AMI_1:81;
A23: Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(0 + 1) = Following (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),(Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),0 ) by AMI_1:14
.= Following (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) by AMI_1:13
.= Exec (F₄(),F₅() <=0_goto ((card F₃()) + 2)),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) by A17, I2, SCMPDS_6:22 ;
A24: DataPart ((Initialize t) +* (stop F₃())) = DataPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) by FUNCT_7:134, SCMPDS_4:24;

now

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

end;

then A25: DataPart ((Initialize t) +* (stop F₃())) = DataPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1) by SCMPDS_4:23;
F₃() is_halting_on t by A4, A8, A9, A10;
then A26: ProgramPart ((Initialize t) +* (stop F₃())) halts_on (Initialize t) +* (stop F₃()) by SCMPDS_6:def 3;
I3: (Initialize ((Initialize t) +* (stop F₃()))) +* (stop F₃()) = ((Initialize t) +* (stop F₃())) +* (Initialize (stop F₃())) by SCMPDS_4:5;
(Initialize t) +* (stop F₃()) = (Initialize ((Initialize t) +* (stop F₃()))) +* (stop F₃()) by A18, I3, FUNCT_4:79;
then ProgramPart ((Initialize ((Initialize t) +* (stop F₃()))) +* (stop F₃())) halts_on (Initialize ((Initialize t) +* (stop F₃()))) +* (stop F₃()) by A26;
then A27: F₃() is_halting_on (Initialize t) +* (stop F₃()) by SCMPDS_6:def 3;
A28: IExec F₃(),t = (Result (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (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 (Initialize t) +* (stop F₃()) by SCMPDS_6:38;
not F₄() in dom (Initialize (stop (while>0 F₄(),F₅(),F₃()))) by SCMPDS_4:31;
then ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) . (DataLoc (((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) . F₄()),F₅()) = ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) . (DataLoc (F₂() . F₄()),F₅()) by A9, I2, FUNCT_4:12
.= t . (DataLoc (F₂() . F₄()),F₅()) by A16, I2, FUNCT_4:12 ;
then A32: IC (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1) = succ (IC ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))) by A10, A23, SCMPDS_2:68
.= 0 + 1 by A19 ;
then A33: IC (Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1),(LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃())))) = (card F₃()) + 1 by A1, A18, A27, A31, A25, A22, SCMPDS_7:36;
Y: (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1))) /. (IC (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1))) = (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1)) . (IC (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1))) by COMPOS_1:38;
ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) = ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1) by AMI_1:123;
then A34: Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) = Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1),(LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) by AMI_1:51;
then A35: CurInstr (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1))),(Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1)) = (Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1),(LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃())))) . ((card F₃()) + 1) by A1, A18, A27, A31, A32, A25, A22, Y, SCMPDS_7:36
.= (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1) . ((card F₃()) + 1) by AMI_1:54
.= ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) . ((card F₃()) + 1) by AMI_1:54
.= (while>0 F₄(),F₅(),F₃()) . ((card F₃()) + 1) by A20, A21, GRFUNC_1:8
.= goto (- ((card F₃()) + 1)) by Th19 ;
T: ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) = ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1)) by AMI_1:123;
A36: Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1) = Following (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),(Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1)) by AMI_1:14
.= Exec (goto (- ((card F₃()) + 1))),(Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1)) by A35, T ;
then IC (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1)) = ICplusConst (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1)),(0 - ((card F₃()) + 1)) by SCMPDS_2:66
.= 0 by A33, A34, SCMPDS_7:1 ;
then A37: (Initialize (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1))) +* (stop (while>0 F₄(),F₅(),F₃())) = Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1) by SCMPDS_7:37;
A38: DataPart (Comput (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃())),(LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃())))) = DataPart (Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1),(LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃())))) by A1, A18, A27, A31, A32, A25, A22, SCMPDS_7:36;
then A39: DataPart (Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1),(LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃())))) = DataPart (Result (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) by A26, AMI_1:122
.= DataPart ((Result (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (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 (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1)) = Dstate (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (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 (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1)))) < k + 1 by A7, A40, XXREAL_0:2;
assume F₁((Dstate (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1)))) > k ; :: thesis: contradiction
hence contradiction by A42, INT_1:20; :: thesis: verum

end;

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

now

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

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

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

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

hereby :: thesis: verum

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

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

hence IC (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (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 (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (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 (Comput (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃())),kn) as Element of NAT ;
t: ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) = ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1) by AMI_1:123;
kn < k by A48, XREAL_1:31;
then kn < LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃())) by A47, XXREAL_0:2;
then (IC (Comput (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃())),kn)) + 1 = IC (Comput (ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1)),(Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),1),kn) by A1, A18, A27, A31, A32, A25, A22, SCMPDS_7:34;
then A49: IC (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),k) = lm + 1 by A48, t, AMI_1:51;
IC (Comput (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃())),kn) in dom (stop F₃()) by A30, SCMPDS_6:def 2;
then lm < card (stop F₃()) by AFINSQ_1:70;
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 (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),k) in dom (stop (while>0 F₄(),F₅(),F₃())) by A49, AFINSQ_1:70; :: thesis: verum

end;

end;

end;

end;

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

(card F₃()) + 1 in dom (stop (while>0 F₄(),F₅(),F₃())) by A20, SCMPDS_6:18;
hence IC (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (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 (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1 ; :: thesis: IC (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (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 (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1) + nn by NAT_1:10;
T: ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) = ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1)) by AMI_1:123;
A53: nn in NAT by ORDINAL1:def 13;
then Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),k = Comput (ProgramPart ((Initialize (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1))) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1))) +* (stop (while>0 F₄(),F₅(),F₃()))),nn by A37, A52, T, AMI_1:51;
hence IC (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (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 Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1) by A6, A29, A44, A40, A41;
then ProgramPart (Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1)) halts_on Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1) by A37, SCMPDS_6:def 3;
then ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) halts_on Comput (ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())))),((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))),(((LifeSpan (ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) + 1) + 1) by AMI_1:123;
then ProgramPart ((Initialize t) +* (stop (while>0 F₄(),F₅(),F₃()))) halts_on (Initialize t) +* (stop (while>0 F₄(),F₅(),F₃())) 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