set b = DataLoc ((F₁() . F₃()),F₄());
set FR = for-down (F₃(),F₄(),F₅(),F₂());
defpred S₁[ Nat] means for t being State of SCMPDS st t . (DataLoc ((F₁() . F₃()),F₄())) <= $1 & t . F₃() = F₁() . F₃() & P₁[ Dstate t] holds
( (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),t)) . (DataLoc ((F₁() . F₃()),F₄())) <= 0 & P₁[ Dstate (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),t))] );
A4: S₁[ 0 ]

proof

let t be State of SCMPDS; :: thesis: ( t . (DataLoc ((F₁() . F₃()),F₄())) <= 0 & t . F₃() = F₁() . F₃() & P₁[ Dstate t] implies ( (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),t)) . (DataLoc ((F₁() . F₃()),F₄())) <= 0 & P₁[ Dstate (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),t))] ) )
assume that
A5: ( t . (DataLoc ((F₁() . F₃()),F₄())) <= 0 & t . F₃() = F₁() . F₃() ) and
A6: P₁[ Dstate t] ; :: thesis: ( (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),t)) . (DataLoc ((F₁() . F₃()),F₄())) <= 0 & P₁[ Dstate (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),t))] )
thus (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),t)) . (DataLoc ((F₁() . F₃()),F₄())) <= 0 by A5, SCMPDS_7:66; :: thesis: P₁[ Dstate (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),t))]
for x being Int_position holds (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),t)) . x = t . x by A5, SCMPDS_7:66;
hence P₁[ Dstate (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),t))] by A6, Th5; :: thesis: verum

end;

A7: now

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

now

let u be State of SCMPDS; :: thesis: ( u . (DataLoc ((F₁() . F₃()),F₄())) <= k + 1 & u . F₃() = F₁() . F₃() & P₁[ Dstate u] implies ( (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),b₁)) . (DataLoc ((F₁() . F₃()),F₄())) <= 0 & P₁[ Dstate (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),b₁))] ) )
assume that
A9: u . (DataLoc ((F₁() . F₃()),F₄())) <= k + 1 and
A10: u . F₃() = F₁() . F₃() and
A11: P₁[ Dstate u] ; :: thesis: ( (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),b₁)) . (DataLoc ((F₁() . F₃()),F₄())) <= 0 & P₁[ Dstate (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),b₁))] )

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₂())),b₁)) . (DataLoc ((F₁() . F₃()),F₄())) <= 0 & P₁[ Dstate (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),b₁))] )

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

end;

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

set Ad = AddTo (F₃(),F₄(),(- F₅()));
set Iu = IExec ((F₂() ';' (AddTo (F₃(),F₄(),(- F₅())))),u);
A13: ( (IExec ((F₂() ';' (AddTo (F₃(),F₄(),(- F₅())))),u)) . F₃() = F₁() . F₃() & P₁[ Dstate (IExec ((F₂() ';' (AddTo (F₃(),F₄(),(- F₅())))),u))] ) by A3, A10, A11, A12;
(IExec ((F₂() ';' (AddTo (F₃(),F₄(),(- F₅())))),u)) . (DataLoc ((F₁() . F₃()),F₄())) = (u . (DataLoc ((F₁() . F₃()),F₄()))) - F₅() by A3, A10, A11, A12;
then ((IExec ((F₂() ';' (AddTo (F₃(),F₄(),(- F₅())))),u)) . (DataLoc ((F₁() . F₃()),F₄()))) + 1 <= u . (DataLoc ((F₁() . F₃()),F₄())) by A1, INT_1:20, XREAL_1:46;
then ((IExec ((F₂() ';' (AddTo (F₃(),F₄(),(- F₅())))),u)) . (DataLoc ((F₁() . F₃()),F₄()))) + 1 <= k + 1 by A9, XXREAL_0:2;
then A14: (IExec ((F₂() ';' (AddTo (F₃(),F₄(),(- F₅())))),u)) . (DataLoc ((F₁() . F₃()),F₄())) <= k by XREAL_1:8;
A15: P₁[ Dstate u] by A11;
A16: for t being State of SCMPDS st P₁[ Dstate t] & t . F₃() = u . F₃() & t . (DataLoc ((u . F₃()),F₄())) > 0 holds
( (IExec ((F₂() ';' (AddTo (F₃(),F₄(),(- F₅())))),t)) . F₃() = t . F₃() & (IExec ((F₂() ';' (AddTo (F₃(),F₄(),(- F₅())))),t)) . (DataLoc ((u . F₃()),F₄())) = (t . (DataLoc ((u . F₃()),F₄()))) - F₅() & F₂() is_closed_on t & F₂() is_halting_on t & P₁[ Dstate (IExec ((F₂() ';' (AddTo (F₃(),F₄(),(- F₅())))),t))] ) by A3, A10;
A17: u . (DataLoc ((u . F₃()),F₄())) > 0 by A10, A12;
( ( P₁[u] or not P₁[u] ) & IExec ((for-down (F₃(),F₄(),F₅(),F₂())),u) = IExec ((for-down (F₃(),F₄(),F₅(),F₂())),(IExec ((F₂() ';' (AddTo (F₃(),F₄(),(- F₅())))),u))) ) from SCPISORT:sch 2(A1, A17, A15, A16);
hence ( (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),u)) . (DataLoc ((F₁() . F₃()),F₄())) <= 0 & P₁[ Dstate (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),u))] ) by A8, A14, A13; :: thesis: verum

end;

end;

end;

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

end;

A18: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A7);
thus ( P₁[F₁()] or not P₁[F₁()] ) ; :: thesis: ( (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),F₁())) . (DataLoc ((F₁() . F₃()),F₄())) <= 0 & P₁[ Dstate (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),F₁()))] )

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₁())) . (DataLoc ((F₁() . F₃()),F₄())) <= 0 & P₁[ Dstate (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),F₁()))] )

then reconsider m = F₁() . (DataLoc ((F₁() . F₃()),F₄())) as Element of NAT by INT_1:16;
S₁[m] by A18;
hence ( (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),F₁())) . (DataLoc ((F₁() . F₃()),F₄())) <= 0 & P₁[ Dstate (IExec ((for-down (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₁())) . (DataLoc ((F₁() . F₃()),F₄())) <= 0 & P₁[ Dstate (IExec ((for-down (F₃(),F₄(),F₅(),F₂())),F₁()))] )

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

end;

end;