Verbose proof for STAB.

STAB:

{1} ∀ (i: nat, n: nat): st(i, v) ≥ n ⊃ st(i + 1, v) ≥ n

Skolemizing,

STAB:

{1} st(i′, v) ≥ n′ ⊃ st(i′ + 1, v) ≥ n′

Applying disjunctive simplification to flatten sequent,

STAB:

\begin{matrix}\{-1\} & st(i′, v) ≥ n′ \\ \{1\} & st(i′ + 1, v) ≥ n′ \end{matrix}

Using n_{0} to name and replace st(i′, v),

STAB:

\begin{matrix}\{-1\} & st(i′, v) = n_{0} \\ \{-2\} & n_{0} ≥ n′ \\ \{1\} & st(i′ + 1, v) ≥ n′ \end{matrix}

Forward chaining on NEXT, we get 2 subgoals:

STAB.1:

\begin{matrix}\{-1\} & st(i′ + 1, v) = n_{0} \\ \{-2\} & st(i′, v) = n_{0} \\ \{-3\} & n_{0} ≥ n′ \\ \{1\} & st(i′ + 1, v) ≥ n′ \end{matrix}

Trying repeated skolemization, instantiation, and if-lifting, This completes the proof of STAB.1.

STAB.2:

{-1} st(i′ + 1, v) > n_{0}
{-2} S(st(i′ + 1, v))
{-3} st(i′, v) = n_{0}
{-4} n_{0} ≥ n′
{1} st(i′ + 1, v) ≥ n′

Trying repeated skolemization, instantiation, and if-lifting, This completes the proof of STAB.2. Q.E.D.