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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(all≤(x, m, n, a) ↔ ¬ a < x[m] ∧ all≤(x, m + 1, n, a)), m < # x, m < n ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  x ≠ [], m < # x, m < n ⊦ (∀ n0. m ≤ n0 ∧ n0 < n ∧ n0 < # x → ¬ a < x[n0]) ↔ ¬ a < x[m] ∧ (∀ n0. m < n0 ∧ n0 < n ∧ n0 < # x → ¬ a < x[n0])

Rule argument

Additional information

Used simplifier rules: allle-range-def: ⊦ all≤(x, m, n, a) ↔ (∀ n0. m ≤ n0 ∧ n0 < n ∧ n0 < # x → ¬ a < x[n0]); ⊦ m < n → n ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (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 + 1 ≤ n ↔ m < n; (s)

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

Heuristic pl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 4:

  x ≠ [], m < n, m < # x, ∀ n0. m ≤ n0 ∧ n0 < n ∧ n0 < # x → ¬ a < x[n0] ⊦ ¬ a < x[m] ∧ (∀ n0. m < n0 ∧ n0 < n ∧ n0 < # x → ¬ a < x[n0])

• Proof step 9:

  x ≠ [], m < n, m < # x, ¬ a < x[m], ∀ n0. m < n0 ∧ n0 < n ∧ n0 < # x → ¬ a < x[n0] ⊦ ∀ n0. m ≤ n0 ∧ n0 < n ∧ n0 < # x → ¬ a < x[n0]

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  x ≠ [], m < # x, m < n, ∀ n0. m ≤ n0 ∧ n0 < n ∧ n0 < # x → ¬ a < x[n0] ⊦ ¬ a < x[m] ∧ (m < n0 ∧ n0 < n ∧ n0 < # x → ¬ a < x[n0])

Rule argument

Additional information

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

Heuristic pl case distinction applied rule case distinction

And obtained the following new goals

• Proof step 6:

  x ≠ [], a < x[m], m < n, m < # x, ∀ n0. m ≤ n0 ∧ n0 < n ∧ n0 < # x → ¬ a < x[n0] ⊦

• Proof step 7:

  x ≠ [], a < x[n0], m < n0, n0 < n, n0 < # x, m < n, m < # x, ∀ n0. m ≤ n0 ∧ n0 < n ∧ n0 < # x → ¬ a < x[n0] ⊦

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (s) Used terms: m

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  x ≠ [], a < x[n0], m < n0, n0 < n, n0 < # x, m < n, m < # x, m + 1 < n, m + 1 < # x, ∀ n0. m ≤ n0 ∧ n0 < n ∧ n0 < # x → ¬ a < x[n0] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 8 from proof alllerange-reclow (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 → m ≤ n; (s) Used terms: n0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  x ≠ [], a < x[n0], n0 < n, n0 < # x, x[m] < x[n0], m < n, m < # x, m ≤ n0, ¬ a < x[m], ∀ n0. m < n0 ∧ n0 < n ∧ n0 < # x → ¬ a < x[n0] ⊦

Rule argument

Additional information

Used simplifier rules: nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification weakord[tord] fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat

Proof step 10 from proof alllerange-reclow (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; (ss) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) Used terms: n0