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
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st F₁((Dstate t)) <= $1 & t . F₅() = F₂() . F₅() & P₁[ Dstate t] holds
( F₁((Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),Q,t)))) = 0 & P₁[ Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),Q,t))] );
A5: S₁[ 0 ]

proof

let t be State of SCMPDS; :: thesis: for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st F₁((Dstate t)) <= 0 & t . F₅() = F₂() . F₅() & P₁[ Dstate t] holds
( F₁((Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),Q,t)))) = 0 & P₁[ Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),Q,t))] )
let Q be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: ( F₁((Dstate t)) <= 0 & t . F₅() = F₂() . F₅() & P₁[ Dstate t] implies ( F₁((Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),Q,t)))) = 0 & P₁[ Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),Q,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₄())),Q,t)))) = 0 & P₁[ Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),Q,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₄())),Q,t)) . b = t . b by A7, SCMPDS_8:12;
hence ( F₁((Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),Q,t)))) = 0 & P₁[ Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),Q,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: for U being the Instructions of SCMPDS -valued ManySortedSet of NAT st F₁((Dstate u)) <= k + 1 & u . F₅() = F₂() . F₅() & P₁[ Dstate u] holds
( F₁((Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),b₃,b₂)))) = 0 & P₁[ Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),b₃,b₂))] )
let U be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: ( F₁((Dstate u)) <= k + 1 & u . F₅() = F₂() . F₅() & P₁[ Dstate u] implies ( F₁((Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),b₂,b₁)))) = 0 & P₁[ Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),b₂,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₂,b₁)))) = 0 & P₁[ Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),b₂,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₂,b₁)))) = 0 & P₁[ Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),b₂,b₁))] )

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

end;

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

set Iu = IExec (F₄(),U,u);
A16: u . (DataLoc ((F₂() . F₅()),F₆())) < 0 by A2, A14, A15;
then A17: ( (IExec (F₄(),U,u)) . F₅() = F₂() . F₅() & P₁[ Dstate (IExec (F₄(),U,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,u))) < H₁( Dstate u) by A4, A13, A14, A16;
then H₁( Dstate (IExec (F₄(),U,u))) + 1 <= H₁( Dstate u) by INT_1:20;
then H₁( Dstate (IExec (F₄(),U,u))) + 1 <= k + 1 by A12, XXREAL_0:2;
then A20: H₁( Dstate (IExec (F₄(),U,u))) <= k by XREAL_1:8;
A21: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st P₁[ Dstate t] & t . F₅() = u . F₅() & t . (DataLoc ((u . F₅()),F₆())) < 0 holds
( (IExec (F₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & H₁( Dstate (IExec (F₄(),Q,t))) < H₁( Dstate t) & P₁[ Dstate (IExec (F₄(),Q,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,u) = IExec ((while<0 (F₅(),F₆(),F₄())),U,(IExec (F₄(),U,u))) ) from SCMPDS_8:sch 2(A22, A19, A18, A21);
hence ( H₁( Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),U,u))) = 0 & P₁[ Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),U,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₃(),F₂())))) = 0 & P₁[ Dstate (IExec ((while<0 (F₅(),F₆(),F₄())),F₃(),F₂()))] ) by A3; :: thesis: verum