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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ⌜n⌝ < # σσ, mon(σσ), m ≤ n, ¬ σσ[m] ⊑ σσ[n] ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ⌜n⌝ < # σσ, mon(σσ), m ≤ n, ¬ σσ[m] ⊑ σσ[n] ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  n1 +1 = n - m, ⌜n⌝ < # σσ, mon(σσ), m ≤ n, ¬ σσ[m] ⊑ σσ[n], ∀ n, m, σσ. ¬(n1 = n - m ∧ ⌜n⌝ < # σσ ∧ mon(σσ) ∧ m ≤ n ∧ ¬ σσ[m] ⊑ σσ[n]) ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; ⊦ m ≤ n → (n - m = 0 ↔ n = m); (s) ⊦ m ≤ m; (s) ⊦ σ ⊑ σ; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  n1 + 1 = n - m, ⌜n⌝ < # σσ, mon(σσ), m ≤ n, ¬ σσ[m] ⊑ σσ[n], ∀ n0, m0, σσ0. n1 ≠ n0 - m0 ∨ ¬ ⌜n0⌝ < # σσ0 ∨ ¬ mon(σσ0) ∨ ¬ m0 ≤ n0 ∨ σσ0[m0] ⊑ σσ0[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  n1 + 1 = n2, n = n2 + m, ⌜n⌝ < # σσ, mon(σσ), m ≤ n, ¬ σσ[m] ⊑ σσ[n], ∀ n0, m0, σσ0. n1 ≠ n0 - m0 ∨ ¬ ⌜n0⌝ < # σσ0 ∨ ¬ mon(σσ0) ∨ ¬ m0 ≤ n0 ∨ σσ0[m0] ⊑ σσ0[n0] ⊦

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n, m, n2

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ⌜n1⌝ + ⌜1⌝ + ⌜m⌝ < # σσ, mon(σσ), ¬ σσ[m] ⊑ σσ[(n1 + 1) + m], ∀ n0, m0, σσ0. n1 ≠ n0 - m0 ∨ ¬ ⌜n0⌝ < # σσ0 ∨ ¬ mon(σσ0) ∨ ¬ m0 ≤ n0 ∨ σσ0[m0] ⊑ σσ0[n0] ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ m ≤ m + n; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 8:

  ⌜n1⌝ + ⌜1⌝ + ⌜m⌝ < # σσ, mon(σσ), ¬ σσ[m] ⊑ σσ[(n1 + 1) + m], n1 ≠ n1 + m - m ∨ ¬ ⌜n1 + m⌝ < # σσ ∨ ¬ mon(σσ) ∨ ¬ m ≤ n1 + m ∨ σσ[m] ⊑ σσ[n1 + m] ⊦

Rule argument

Additional information

Used terms: n1 + m, m, σσ

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ⌜n1⌝ + ⌜1⌝ + ⌜m⌝ < # σσ, ⌜n1⌝ + ⌜m⌝ < # σσ, mon(σσ), σσ[m] ⊑ σσ[n1 + m], ¬ σσ[m] ⊑ σσ[(n1 + 1) + m] ⊦

Rule argument

Additional information

Used simplifier rules: 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 c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ¬ m + n < m; (s) ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n + m < n0; (s) ⊦ ⌜n⌝ + n∞1 < ⌜n⌝ + n∞2 ↔ n∞1 < n∞2; (s) lsle-trans: ⊦ n∞ < n∞1 ∧ ¬ n∞2 < n∞1 → n∞ < n∞2; (forward) from specification nat-inf ⊦ m ≤ m + n; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ m + n - m = n; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  ⌜n1⌝ + ⌜m⌝ < # σσ, ⌜n1⌝ + ⌜1⌝ + ⌜m⌝ < # σσ, σσ[m] ⊑ σσ[n1 + m], ¬ σσ[m] ⊑ σσ[(n1 + 1) + m], ∀ n. ⌜n⌝ + ⌜1⌝ < # σσ → σσ[n] ⊑ σσ[n + 1] ⊦

Rule argument

Additional information

Used terms: σσ

Proof step 10 from proof mon-lem (previous step) (back to tree)

Lemma mon-def

Proof step 11 from proof mon-lem (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic 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 leq-trans: ⊦ σ ⊑ σ1 ∧ σ1 ⊑ σ2 → σ ⊑ σ2; (forward) from specification stream Used terms: n1 + m