set b = DataLoc ((F₂() . F₄()),F₅());
set WHL = while>0 (F₄(),F₅(),F₃());
defpred S₁[ Element of NAT ] means for t being State of SCMPDS st F₁((Dstate t)) <= $1 & t . F₄() = F₂() . F₄() & P₁[ Dstate t] holds
( F₁((Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),t)))) = 0 & P₁[ Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),t))] );
A5: S₁[ 0 ]

proof

let t be State of SCMPDS; :: thesis: ( F₁((Dstate t)) <= 0 & t . F₄() = F₂() . F₄() & P₁[ Dstate t] implies ( F₁((Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),t)))) = 0 & P₁[ Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),t))] ) )
assume that
A6: F₁((Dstate t)) <= 0 and
A7: t . F₄() = F₂() . F₄() and
A8: P₁[ Dstate t] ; :: thesis: ( F₁((Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),t)))) = 0 & P₁[ Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),t))] )
F₁((Dstate t)) >= 0 by NAT_1:2;
then A9: F₁((Dstate t)) = 0 by A6, XXREAL_0:1;
then t . (DataLoc ((F₂() . F₄()),F₅())) <= 0 by A2, A8;
then for b being Int_position holds (IExec ((while>0 (F₄(),F₅(),F₃())),t)) . b = t . b by A7, SCMPDS_8:23;
hence ( F₁((Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),t)))) = 0 & P₁[ Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),t))] ) by A8, A9, SCPISORT:5; :: thesis: verum

end;

A10: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A11: S₁[k] ; :: thesis: S₁[k + 1]

now

let u be State of SCMPDS; :: thesis: ( F₁((Dstate u)) <= k + 1 & u . F₄() = F₂() . F₄() & P₁[ Dstate u] implies ( F₁((Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),b₁)))) = 0 & P₁[ Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),b₁))] ) )
assume that
A12: F₁((Dstate u)) <= k + 1 and
A13: u . F₄() = F₂() . F₄() and
A14: P₁[ Dstate u] ; :: thesis: ( F₁((Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),b₁)))) = 0 & P₁[ Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),b₁))] )

per cases ( F₁((Dstate u)) = 0 or F₁((Dstate u)) <> 0 ) ;

suppose F₁((Dstate u)) = 0 ; :: thesis: ( F₁((Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),b₁)))) = 0 & P₁[ Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),b₁))] )

hence ( F₁((Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),u)))) = 0 & P₁[ Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),u))] ) by A5, A13, A14; :: thesis: verum

end;

suppose A15: F₁((Dstate u)) <> 0 ; :: thesis: ( H₁( Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),b₁))) = 0 & P₁[ Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),b₁))] )

set Iu = IExec (F₃(),u);
A16: u . (DataLoc ((F₂() . F₄()),F₅())) > 0 by A2, A14, A15;
then A17: ( (IExec (F₃(),u)) . F₄() = F₂() . F₄() & P₁[ Dstate (IExec (F₃(),u))] ) by A4, A13, A14;
deffunc H₁( State of SCMPDS) -> Element of NAT = F₁($1);
A18: P₁[ Dstate u] by A14;
A19: for t being State of SCMPDS st P₁[ Dstate t] & H₁( Dstate t) = 0 holds
t . (DataLoc ((u . F₄()),F₅())) <= 0 by A2, A13;
H₁( Dstate (IExec (F₃(),u))) < H₁( Dstate u) by A4, A13, A14, A16;
then H₁( Dstate (IExec (F₃(),u))) + 1 <= H₁( Dstate u) by INT_1:20;
then H₁( Dstate (IExec (F₃(),u))) + 1 <= k + 1 by A12, XXREAL_0:2;
then A20: H₁( Dstate (IExec (F₃(),u))) <= k by XREAL_1:8;
A21: for t being State of SCMPDS st P₁[ Dstate t] & t . F₄() = u . F₄() & t . (DataLoc ((u . F₄()),F₅())) > 0 holds
( (IExec (F₃(),t)) . F₄() = t . F₄() & F₃() is_closed_on t & F₃() is_halting_on t & H₁( Dstate (IExec (F₃(),t))) < H₁( Dstate t) & P₁[ Dstate (IExec (F₃(),t))] ) by A4, A13;
A22: u . (DataLoc ((u . F₄()),F₅())) > 0 by A2, A13, A14, A15;
( ( H₁(u) = H₁(u) or P₁[u] ) & IExec ((while>0 (F₄(),F₅(),F₃())),u) = IExec ((while>0 (F₄(),F₅(),F₃())),(IExec (F₃(),u))) ) from SCMPDS_8:sch 4(A1, A22, A19, A18, A21);
hence ( H₁( Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),u))) = 0 & P₁[ Dstate (IExec ((while>0 (F₄(),F₅(),F₃())),u))] ) by A11, A20, A17; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

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