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₁[ 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, Th16; :: 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 COMPOS_1:135;
A15: dom (ProgramPart t) = NAT by COMPOS_1:34;
A16: while<>0 (F₄(),F₅(),F₃()) = ((F₄(),F₅()) <>0_goto 2) ';' (((goto ((card F₃()) + 2)) ';' F₃()) ';' (goto (- ((card F₃()) + 2)))) by Lm10;
A17: not DataLoc ((F₂() . F₄()),F₅()) in dom (Initialize (stop (while<>0 (F₄(),F₅(),F₃())))) by SCMPDS_4:31;
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);
I2: (Initialize t) +* (stop F₃()) = t +* (Initialize (stop F₃())) by COMPOS_1:125;
I3: (Initialize t) +* (stop (while<>0 (F₄(),F₅(),F₃()))) = t +* (Initialize (stop (while<>0 (F₄(),F₅(),F₃())))) by COMPOS_1:125;
A18: Initialize (stop F₃()) c= (Initialize t) +* (stop F₃()) by I2, 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 l2 = (card F₃()) + 2;
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₃()) + 2 < (card F₃()) + 3 by XREAL_1:8;
then A20: (card F₃()) + 2 in dom (while<>0 (F₄(),F₅(),F₃())) by Th13;
( 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 I3, 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₃(),2) c= while<>0 (F₄(),F₅(),F₃()) by Lm11;
then Shift (F₃(),2) c= (Initialize t) +* (stop (while<>0 (F₄(),F₅(),F₃()))) by A21, XBOOLE_1:1;
then A22: Shift (F₃(),2) 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 EXTPRO_1:4
.= Following ((ProgramPart ((Initialize t) +* (stop (while<>0 (F₄(),F₅(),F₃()))))),((Initialize t) +* (stop (while<>0 (F₄(),F₅(),F₃()))))) by EXTPRO_1:3
.= Exec (((F₄(),F₅()) <>0_goto 2),((Initialize t) +* (stop (while<>0 (F₄(),F₅(),F₃()))))) by A16, I3, SCMPDS_6:22 ;
A24: DataPart ((Initialize t) +* (stop F₃())) = DataPart ((Initialize t) +* (stop (while<>0 (F₄(),F₅(),F₃())))) by COMPOS_1:138, FUNCT_7:134;

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:67 ; :: 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;
I4: (Initialize ((Initialize t) +* (stop F₃()))) +* (stop F₃()) = ((Initialize t) +* (stop F₃())) +* (Initialize (stop F₃())) by COMPOS_1:125;
(Initialize t) +* (stop F₃()) = (Initialize ((Initialize t) +* (stop F₃()))) +* (stop F₃()) by A18, I4, 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, I3, FUNCT_4:12
.= t . (DataLoc ((F₂() . F₄()),F₅())) by A17, I3, 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)) = ICplusConst (((Initialize t) +* (stop (while<>0 (F₄(),F₅(),F₃())))),2) by A10, A23, SCMPDS_2:67
.= 0 + 2 by A19, SCMPDS_6:23 ;
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₃()) + 2 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 EXTPRO_1:5;
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₃()) + 2) 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₃()) + 2) by AMI_1:54
.= ((Initialize t) +* (stop (while<>0 (F₄(),F₅(),F₃())))) . ((card F₃()) + 2) by AMI_1:54
.= (while<>0 (F₄(),F₅(),F₃())) . ((card F₃()) + 2) by A20, A21, GRFUNC_1:8
.= goto (- ((card F₃()) + 2)) by Th15 ;
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 EXTPRO_1:4
.= Exec ((goto (- ((card F₃()) + 2))),(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₃()) + 2))) 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, EXTPRO_1:23
.= 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₃()) + 2))) = 0 by SCMPDS_2:21;
then InsCode (goto (- ((card F₃()) + 2))) 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, SCMPDS_8:3
.= Dstate (IExec (F₃(),t)) by A39, A34, SCMPDS_8:2 ;

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, EXTPRO_1:23
.= 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, EXTPRO_1:5 ;
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, EXTPRO_1:3; :: 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))) + 2 = 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 + 2 by A48, t, EXTPRO_1:5;
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 + 2 < ((card F₃()) + 1) + 2 by XREAL_1:8;
(card F₃()) + 3 < (card F₃()) + 4 by XREAL_1:8;
then lm + 2 < (card F₃()) + 4 by A50, XXREAL_0:2;
then lm + 2 < card (stop (while<>0 (F₄(),F₅(),F₃()))) by Lm9;
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₃()) + 2 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;
reconsider nn = nn as Element of NAT by ORDINAL1:def 13;
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;
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, EXTPRO_1:5;
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, 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 EXTPRO_1:22;
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₂()));
A53: 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
A54: ( F₁((Dstate t)) <= 0 & P₁[ Dstate t] ) and
A55: 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 NAT_1:2;
then t . (DataLoc ((F₂() . F₄()),F₅())) = 0 by A2, A54, XXREAL_0:1;
hence ( while<>0 (F₄(),F₅(),F₃()) is_closed_on t & while<>0 (F₄(),F₅(),F₃()) is_halting_on t ) by A55, Th16; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A53, 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