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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(mon<(⌜nnf to n⌝ ) ↔ true), mon<(⌜nnf⌝ ) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  mon<(⌜nnf⌝ ), ¬ mon<(⌜nnf to n⌝ ) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ mon<(nσ) ↔ (∀ n. ⌜n⌝ + ⌜1⌝ < # nσ → nσ[n] < nσ[n + 1])

• Proof step 5:

  mon<(⌜nnf⌝ ), ∃ n0. ¬(⌜n0⌝ + ⌜1⌝ < # ⌜nnf to n⌝ → ⌜nnf to n⌝ [n0] < ⌜nnf to n⌝ [n0 + 1]) ⊦

Rule argument

Additional information

Used terms: ⌜nnf to n⌝

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

Lemma monls-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  n0 + 1 < n, mon<(⌜nnf⌝ ), nnf(n0 + 1) ≤ nnf(n0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n ↔ ¬ n ≤ m; (ss) m < n ⊦ (nf to n)[m] = nf(m); (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ ⌜x⌝ [n] = x[n]; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ¬ m + n < m; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat 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) ⊦ # ⌜nf to n⌝ = ⌜n⌝ ; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ mon<(nσ) ↔ (∀ n. ⌜n⌝ + ⌜1⌝ < # nσ → nσ[n] < nσ[n + 1])

• Proof step 8:

  n0 + 1 < n, nnf(n0 + 1) ≤ nnf(n0), ∀ n. ⌜n⌝ + ⌜1⌝ < # ⌜nnf⌝ → ⌜nnf⌝ [n] < ⌜nnf⌝ [n + 1] ⊦

Rule argument

Additional information

Used terms: ⌜nnf⌝

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

Lemma monls-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  n0 + 1 < n, nnf(n0 + 1) ≤ nnf(n0), ∀ n1. nnf(n1) < nnf(n1 + 1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ [n] = nf(n); (s) 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⌝ ≠ ∞; (s) ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞; (s) ⊦ n∞ < ∞ ↔ n∞ ≠ ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s)

Proof step 9 from proof monls-to (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: n0