set b = DataLoc ((F₁() . F₄()),F₅());
set FR = for-down (F₄(),F₅(),F₆(),F₂());
defpred S₁[ Nat] means for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . (DataLoc ((F₁() . F₄()),F₅())) <= $1 & t . F₄() = F₁() . F₄() & P₁[t] holds
( (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),Q,t)) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & P₁[ Initialize (IExec ((for-down (F₄(),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 t . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & t . F₄() = F₁() . F₄() & P₁[t] holds
( (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),Q,t)) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),Q,t))] )
let Q be Instruction-Sequence of SCMPDS; :: thesis: ( t . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & t . F₄() = F₁() . F₄() & P₁[t] implies ( (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),Q,t)) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),Q,t))] ) )
assume that
A5: ( t . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & t . F₄() = F₁() . F₄() ) and
A6: P₁[t] ; :: thesis: ( (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),Q,t)) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),Q,t))] )
A7: Initialize t = t by MEMSTR_0:44;
hence (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),Q,t)) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 by A5, SCMPDS_7:47; :: thesis: P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),Q,t))]
for x being Int_position holds (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),Q,t)) . x = t . x by A5, A7, SCMPDS_7:47;
hence P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),Q,t))] by A6, Th4, A7; :: thesis: verum

end;

A8: 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 A9: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

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

per cases ( u . (DataLoc ((F₁() . F₄()),F₅())) <= 0 or u . (DataLoc ((F₁() . F₄()),F₅())) > 0 ) ;

suppose u . (DataLoc ((F₁() . F₄()),F₅())) <= 0 ; :: thesis: ( (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),U,u)) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),U,u))] )

hence ( (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),U,u)) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),U,u))] ) by A4, A11, A12; :: thesis: verum

end;

suppose A13: u . (DataLoc ((F₁() . F₄()),F₅())) > 0 ; :: thesis: ( (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),U,u)) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),U,u))] )

set Ad = AddTo (F₄(),F₅(),(- F₆()));
set Iu = IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),U,u);
A14: ( (IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),U,u)) . F₄() = F₁() . F₄() & P₁[ Initialize (IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),U,u))] ) by A3, A11, A12, A13;
(IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),U,u)) . (DataLoc ((F₁() . F₄()),F₅())) = (u . (DataLoc ((F₁() . F₄()),F₅()))) - F₆() by A3, A11, A12, A13;
then ((IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),U,u)) . (DataLoc ((F₁() . F₄()),F₅()))) + 1 <= u . (DataLoc ((F₁() . F₄()),F₅())) by A1, INT_1:7, XREAL_1:44;
then ((IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),U,u)) . (DataLoc ((F₁() . F₄()),F₅()))) + 1 <= k + 1 by A10, XXREAL_0:2;
then A15: (IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),U,u)) . (DataLoc ((F₁() . F₄()),F₅())) <= k by XREAL_1:6;
A16: P₁[u] by A12;
A17: 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₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),Q,t)) . F₄() = t . F₄() & (IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),Q,t)) . (DataLoc ((u . F₄()),F₅())) = (t . (DataLoc ((u . F₄()),F₅()))) - F₆() & F₂() is_closed_on t,Q & F₂() is_halting_on t,Q & P₁[ Initialize (IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),Q,t))] ) by A3, A11;
A18: u . (DataLoc ((u . F₄()),F₅())) > 0 by A11, A13;
A19: (Initialize (IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),U,u))) . (DataLoc ((F₁() . F₄()),F₅())) = (IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),U,u)) . (DataLoc ((F₁() . F₄()),F₅())) by SCMPDS_5:15;
A20: (Initialize (IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),U,u))) . F₄() = (IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),U,u)) . F₄() by SCMPDS_5:15;
IExec ((for-down (F₄(),F₅(),F₆(),F₂())),U,u) = IExec ((for-down (F₄(),F₅(),F₆(),F₂())),U,(Initialize (IExec ((F₂() ';' (AddTo (F₄(),F₅(),(- F₆())))),U,u)))) from SCPISORT:sch 2(A1, A18, A16, A17);
hence ( (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),U,u)) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),U,u))] ) by A9, A15, A14, A19, A20; :: thesis: verum

end;

end;

end;

end;

A21: for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A8);

per cases ( F₁() . (DataLoc ((F₁() . F₄()),F₅())) > 0 or F₁() . (DataLoc ((F₁() . F₄()),F₅())) <= 0 ) ;

suppose F₁() . (DataLoc ((F₁() . F₄()),F₅())) > 0 ; :: thesis: ( (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),F₃(),F₁())) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),F₃(),F₁()))] )

then reconsider m = F₁() . (DataLoc ((F₁() . F₄()),F₅())) as Element of NAT by INT_1:3;
S₁[m] by A21;
hence ( (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),F₃(),F₁())) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),F₃(),F₁()))] ) by A2; :: thesis: verum

end;

suppose F₁() . (DataLoc ((F₁() . F₄()),F₅())) <= 0 ; :: thesis: ( (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),F₃(),F₁())) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),F₃(),F₁()))] )

hence ( (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),F₃(),F₁())) . (DataLoc ((F₁() . F₄()),F₅())) <= 0 & P₁[ Initialize (IExec ((for-down (F₄(),F₅(),F₆(),F₂())),F₃(),F₁()))] ) by A2, A4; :: thesis: verum

end;

end;