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);
A18: (Initialize t) +* (stop F₃()) = t +* (Initialize (stop F₃())) by COMPOS_1:125;
A19: (Initialize t) +* (stop (while<>0 (F₄(),F₅(),F₃()))) = t +* (Initialize (stop (while<>0 (F₄(),F₅(),F₃())))) by COMPOS_1:125;
A20: Initialize (stop F₃()) c= (Initialize t) +* (stop F₃()) by A18, 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;
A21: 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 A22: (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 A19, FUNCT_4:26, SCMPDS_6:17;
then A23: 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 A23, XBOOLE_1:1;
then A24: 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;
A25: 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, A19, SCMPDS_6:22 ;
A26: 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 A26, SCMPDS_4:23
.= (Comput ((ProgramPart ((Initialize t) +* (stop (while<>0 (F₄(),F₅(),F₃()))))),((Initialize t) +* (stop (while<>0 (F₄(),F₅(),F₃())))),1)) . a by A25, SCMPDS_2:67 ; :: thesis: verum

end;

then A27: 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 A28: ProgramPart ((Initialize t) +* (stop F₃())) halts_on (Initialize t) +* (stop F₃()) by SCMPDS_6:def 3;
A29: (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 A20, A29, FUNCT_4:79;
then ProgramPart ((Initialize ((Initialize t) +* (stop F₃()))) +* (stop F₃())) halts_on (Initialize ((Initialize t) +* (stop F₃()))) +* (stop F₃()) by A28;
then A30: F₃() is_halting_on (Initialize t) +* (stop F₃()) by SCMPDS_6:def 3;
A31: IExec (F₃(),t) = (Result ((ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃())))) +* (t | NAT) by SCMPDS_4:def 8;
A32: P₁[ Dstate (IExec (F₃(),t))] by A4, A8, A9, A10;
A33: F₃() is_closed_on t by A4, A8, A9, A10;
then A34: 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, A19, FUNCT_4:12
.= t . (DataLoc ((F₂() . F₄()),F₅())) by A17, A19, FUNCT_4:12 ;
then A35: 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, A25, SCMPDS_2:67
.= 0 + 2 by A21, SCMPDS_6:23 ;
then A36: 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, A20, A30, A34, A27, A24, SCMPDS_7:36;
A37: (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 A38: 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 A39: 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, A20, A30, A34, A35, A27, A24, A37, 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 A22, A23, GRFUNC_1:8
.= goto (- ((card F₃()) + 2)) by Th15 ;
A40: 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;
A41: 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 A39, A40 ;
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 A36, A38, SCMPDS_7:1 ;
then A42: (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;
A43: 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, A20, A30, A34, A35, A27, A24, SCMPDS_7:36;
then A44: 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 A28, 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 A45: 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 A41, SCMPDS_8:3
.= Dstate (IExec (F₃(),t)) by A44, A38, SCMPDS_8:2 ;

A46: now

F₁((Dstate (IExec (F₃(),t)))) < F₁((Dstate t)) by A4, A8, A9, A10;
then A47: 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, A45, 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 A47, INT_1:20; :: thesis: verum

end;

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

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 A52: 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 A52, NAT_1:8;

suppose A53: 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, A21, 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
A54: 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 ;
A55: 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 A54, XREAL_1:31;
then kn < LifeSpan ((ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃()))) by A53, 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, A20, A30, A34, A35, A27, A24, SCMPDS_7:34;
then A56: IC (Comput ((ProgramPart ((Initialize t) +* (stop (while<>0 (F₄(),F₅(),F₃()))))),((Initialize t) +* (stop (while<>0 (F₄(),F₅(),F₃())))),k)) = lm + 2 by A54, A55, EXTPRO_1:5;
IC (Comput ((ProgramPart ((Initialize t) +* (stop F₃()))),((Initialize t) +* (stop F₃())),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 + 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 A57, 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 A56, AFINSQ_1:70; :: thesis: verum

end;

end;

end;

end;

suppose A58: 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 A22, 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, A20, A30, A34, A35, A27, A24, A38, A58, 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
A59: 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 A42, A59, 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 A51, 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, A32, A50, A45, A46;
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 A42, 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₂()));
A60: 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
A61: ( F₁((Dstate t)) <= 0 & P₁[ Dstate t] ) and
A62: 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, A61, XXREAL_0:1;
hence ( while<>0 (F₄(),F₅(),F₃()) is_closed_on t & while<>0 (F₄(),F₅(),F₃()) is_halting_on t ) by A62, Th16; :: 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₂() & while<>0 (F₄(),F₅(),F₃()) is_halting_on F₂() ) by A3; :: thesis: verum