Proof step 1 from proof succlessleninv-invsize (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(# nσ = ⌜inv(nσ)[n]⌝ + ⌜1⌝ ↔ false), ⌜n⌝ + ⌜1⌝ < leninv(nσ), stutf(nσ) ⊦

Rule argument

Additional information

Proof step 2 from proof succlessleninv-invsize (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # nσ = ⌜inv(nσ)[n]⌝ + ⌜1⌝ , ⌜n⌝ + ⌜1⌝ < leninv(nσ), stutf(nσ) ⊦

Rule argument

Additional information

Proof step 3 from proof succlessleninv-invsize (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  # nσ = ⌜inv(nσ)[n]⌝ + ⌜1⌝ , ⌜n0⌝ = leninv(nσ), ⌜n⌝ + ⌜1⌝ < leninv(nσ), stutf(nσ) ⊦

Rule argument

Additional information

Used simplifier rules: leninv-inf-strong: ⊦ stutf(nσ) → ( leninv(nσ) = ∞ ↔ # nσ = ∞ ∧ (∀ m. ∃ m0. m < m0 ∧ nσ[m] < nσ[m0]) ∧ (∀ m. ∃ m0. m < nσ[m0])); natinf freely generated by ∞, ⌜ ⌝;; add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf ⊦ n∞ = ⌜m⌝ + ⌜n⌝ → (n∞ = ∞ ↔ false); (s)

Proof step 4 from proof succlessleninv-invsize (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # nσ = ⌜inv(nσ)[n]⌝ + ⌜1⌝ , ⌜n0⌝ = leninv(nσ), n + 1 < n0, stutf(nσ) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n + m < n0; (s)

Proof step 5 from proof succlessleninv-invsize (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 6:

  # nσ = ⌜inv(nσ)[n]⌝ + ⌜1⌝ , n0 = n1 +1, ⌜n0⌝ = leninv(nσ), n + 1 < n0, stutf(nσ) ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; n0 < n ⊦ ¬ m + (* n) < (* n0); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 6 from proof succlessleninv-invsize (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # nσ = ⌜inv(nσ)[n]⌝ + ⌜1⌝ , ⌜n1⌝ + ⌜1⌝ = leninv(nσ), n < n1, stutf(nσ) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m +1 = m + 1; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

Proof step 7 from proof succlessleninv-invsize (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 8:

  ⊦ mon<(nσ) ∧ m < n ∧ ⌜n⌝ < # nσ → nσ[m] < nσ[n]

Rule argument

Additional information

Used simplifier rules: stutf-invmonls: ⊦ stutf(nσ) → (mon<(inv(nσ)) ↔ true); leninv-is-len-inv: ⊦ stutf(nσ) → # inv(nσ) = leninv(nσ); leninv-invlast-inv: ⊦ # nσ = ⌜m⌝ + ⌜1⌝ ∧ leninv(nσ) = ⌜n⌝ + ⌜1⌝ ∧ stutf(nσ) → inv(nσ)[n] = m; add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf ⊦ n∞ = ⌜m⌝ + ⌜n0⌝ → (⌜n⌝ < n∞ ↔ n < m + n0); (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ¬ n < n; (s) Used terms: inv(nσ), n, n1

Proof step 8 from proof succlessleninv-invsize (previous step) (back to tree)

Lemma monls-ls