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:12;
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 2(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