set b = DataLoc ((F₂() . F₅()),F₆());
set WHL = while>0 (F₅(),F₆(),F₄());
defpred S₁[ Nat] means for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st F₁(t) <= $1 & t . F₅() = F₂() . F₅() & P₁[t] holds
( F₁((Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),Q,t)))) = 0 & P₁[ Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),Q,t))] );
A4: S₁[ 0 ]

proof

let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st F₁(t) <= 0 & t . F₅() = F₂() . F₅() & P₁[t] holds
( F₁((Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),Q,t)))) = 0 & P₁[ Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),Q,t))] )
let Q be Instruction-Sequence of SCMPDS; :: thesis: ( F₁(t) <= 0 & t . F₅() = F₂() . F₅() & P₁[t] implies ( F₁((Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),Q,t)))) = 0 & P₁[ Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),Q,t))] ) )
A5: Initialize t = t by MEMSTR_0:44;
assume that
A6: F₁(t) <= 0 and
A7: t . F₅() = F₂() . F₅() and
A8: P₁[t] ; :: thesis: ( F₁((Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),Q,t)))) = 0 & P₁[ Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),Q,t))] )
A9: F₁(t) = 0 by A6;
then t . (DataLoc ((F₂() . F₅()),F₆())) <= 0 by A1, A8;
then for b being Int_position holds (IExec ((while>0 (F₅(),F₆(),F₄())),Q,t)) . b = t . b by A7, SCMPDS_8:23;
hence ( F₁((Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),Q,t)))) = 0 & P₁[ Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),Q,t))] ) by A8, A9, A5, SCPISORT:4; :: thesis: verum

end;

A10: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

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

now :: thesis: for u being 0 -started State of SCMPDS
for U being Instruction-Sequence of SCMPDS st F₁(u) <= k + 1 & u . F₅() = F₂() . F₅() & P₁[u] holds
( F₁((Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),U,u)))) = 0 & P₁[ Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),U,u))] )

let u be 0 -started State of SCMPDS; :: thesis: for U being Instruction-Sequence of SCMPDS st F₁(u) <= k + 1 & u . F₅() = F₂() . F₅() & P₁[u] holds
( F₁((Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),b₃,b₂)))) = 0 & P₁[ Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),b₃,b₂))] )
let U be Instruction-Sequence of SCMPDS; :: thesis: ( F₁(u) <= k + 1 & u . F₅() = F₂() . F₅() & P₁[u] implies ( F₁((Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),b₂,b₁)))) = 0 & P₁[ Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),b₂,b₁))] ) )
assume that
A12: F₁(u) <= k + 1 and
A13: u . F₅() = F₂() . F₅() and
A14: P₁[u] ; :: thesis: ( F₁((Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),b₂,b₁)))) = 0 & P₁[ Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),b₂,b₁))] )

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

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

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

end;

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

set Iu = IExec (F₄(),U,u);
A16: u . (DataLoc ((F₂() . F₅()),F₆())) > 0 by A1, A14, A15;
then A17: ( (IExec (F₄(),U,u)) . F₅() = F₂() . F₅() & P₁[ Initialize (IExec (F₄(),U,u))] ) by A3, A13, A14;
deffunc H₁( State of SCMPDS) -> Element of NAT = F₁($1);
A18: P₁[u] by A14;
A19: for t being 0 -started State of SCMPDS st P₁[t] & H₁(t) = 0 holds
t . (DataLoc ((u . F₅()),F₆())) <= 0 by A1, A13;
H₁( Initialize (IExec (F₄(),U,u))) < H₁(u) by A3, A13, A14, A16;
then H₁( Initialize (IExec (F₄(),U,u))) + 1 <= H₁(u) by INT_1:7;
then H₁( Initialize (IExec (F₄(),U,u))) + 1 <= k + 1 by A12, XXREAL_0:2;
then A20: H₁( Initialize (IExec (F₄(),U,u))) <= k by XREAL_1:6;
A21: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P₁[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₁( Initialize (IExec (F₄(),Q,t))) < H₁(t) & P₁[ Initialize (IExec (F₄(),Q,t))] ) by A3, A13;
A22: u . (DataLoc ((u . F₅()),F₆())) > 0 by A1, A13, A14, A15;
A23: IExec ((while>0 (F₅(),F₆(),F₄())),U,u) = IExec ((while>0 (F₅(),F₆(),F₄())),U,(Initialize (IExec (F₄(),U,u)))) from SCMPDS_8:sch 4(A22, A19, A18, A21);
(Initialize (IExec (F₄(),U,u))) . F₅() = (IExec (F₄(),U,u)) . F₅() by SCMPDS_5:15;
hence ( H₁( Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),U,u))) = 0 & P₁[ Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),U,u))] ) by A11, A20, A17, A23; :: thesis: verum

end;

end;

end;

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

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A10);
then S₁[F₁(F₂())] ;
hence ( F₁((Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),F₃(),F₂())))) = 0 & P₁[ Initialize (IExec ((while>0 (F₅(),F₆(),F₄())),F₃(),F₂()))] ) by A2; :: thesis: verum