Proof step 1 from proof ordered-count-splits (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(n < count(x, λ b. b < a) ↔ x[n] < a), n < # x, ordered≤(x) ⊦

Rule argument

Additional information

Proof step 2 from proof ordered-count-splits (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(n < count(x, λ b. b < a) ↔ x[n] < a), x ≠ [], n < # x, ordered≤(x) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 3 from proof ordered-count-splits (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  a0 + x0 ≠ [], ¬(n < count(a0 + x0, λ b. b < a) ↔ (a0 + x0)[n] < a), n < #(a0 + x0), ordered≤(a0 + x0), ∀ n, a. ¬(¬(n < count(x0, λ b. b < a) ↔ x0[n] < a) ∧ x0 ≠ [] ∧ n < # x0 ∧ ordered≤(x0)) ⊦

Rule argument

Additional information

Used simplifier rules: list('a) freely generated by [], +;;

Proof step 4 from proof ordered-count-splits (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ¬(n < (a0 < a ⊃ 1;0) + count(x0, λ b. b < a) ↔ (a0 ' + x0)[n] < a), ordered≤(a0 ' + x0), n ≤ # x0, ∀ n0, a1. (n0 < count(x0, λ b. b < a1) ↔ x0[n0] < a1) ∨ x0 = [] ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ordered≤(a ' + x) → ordered≤(x); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ a + x = a ' + x; (s) ⊦ count(a ' + x, p) = (p(a) ⊃ 1;0) + count(x, p); (s) ⊦ a ' + x ≠ []; (s)

Proof step 5 from proof ordered-count-splits (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 7:

  ¬(n < (a0 < a ⊃ 1;0) + count(x0, λ b. b < a) ↔ (a0 ' + x0)[n] < a), ordered≤(a0 ' + x0), n ≤ # x0, ¬ n < # a0 ', ∀ n0, a1. (n0 < count(x0, λ b. b < a1) ↔ x0[n0] < a1) ∨ x0 = [] ∨ ¬ n0 < # x0 ⊦

• Proof step 18:

  ¬(n < (a0 < a ⊃ 1;0) + count(x0, λ b. b < a) ↔ a0 '[n] < a), n < # a0 ', ordered≤(a0 ' + x0), n ≤ # x0, ∀ n0, a1. (n0 < count(x0, λ b. b < a1) ↔ x0[n0] < a1) ∨ x0 = [] ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used terms: a0 ', x0, n

Proof step 6 from proof ordered-count-splits (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof ordered-count-splits (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ¬(n < (a0 < a ⊃ 1;0) + count(x0, λ b. b < a) ↔ x0[n - 1] < a), n ≠ 0, ordered≤(a0 ' + x0), n ≤ # x0, ∀ n0, a1. (n0 < count(x0, λ b. b < a1) ↔ x0[n0] < a1) ∨ x0 = [] ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < 1 ↔ m = 0; (s) ⊦ # a ' = 0 +1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s)

Proof step 8 from proof ordered-count-splits (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

  n = m + 1, ¬(n < (a0 < a ⊃ 1;0) + count(x0, λ b. b < a) ↔ x0[m] < a), n ≠ 0, ordered≤(a0 ' + x0), n ≤ # x0, ∀ n0, a1. (n0 < count(x0, λ b. b < a1) ↔ x0[n0] < a1) ∨ x0 = [] ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n, m

Proof step 9 from proof ordered-count-splits (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ¬(m + 1 < (a0 < a ⊃ 1;0) + count(x0, λ b. b < a) ↔ x0[m] < a), x0 ≠ [], m < # x0, ordered≤(a0 ' + x0), ∀ n0, a1. (n0 < count(x0, λ b. b < a1) ↔ x0[n0] < a1) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # 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) ⊦ m + 1 ≠ 0; (s)

Proof step 10 from proof ordered-count-splits (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  ¬(m + 1 < (a0 < a ⊃ 1;0) + count(x0, λ b. b < a) ↔ x0[m] < a), x0 ≠ [], m < # x0, ordered≤(a0 ' + x0), (m < count(x0, λ b. b < a) ↔ x0[m] < a) ∨ ¬ m < # x0 ⊦

Rule argument

Additional information

Used terms: m, a

Proof step 11 from proof ordered-count-splits (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  m < count(x0, λ b. b < a) ↔ x0[m] < a, ¬(m + 1 < (a0 < a ⊃ 1;0) + count(x0, λ b. b < a) ↔ x0[m] < a), x0 ≠ [], m < # x0, ordered≤(a0 ' + x0) ⊦

Rule argument

Additional information

Proof step 12 from proof ordered-count-splits (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 13:

  m < count(x0, λ b. b < a) ↔ x0[m] < a, ¬(m + 1 < (a0 < a ⊃ 1;0) + count(x0, λ b. b < a) ↔ x0[m] < a), x0 ≠ [], m < # x0, ordered≤(a0 ' + x0), ¬ a0 < a ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n < m + n0 ↔ n < n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used formulas: a0 < a

Proof step 13 from proof ordered-count-splits (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  m < count(x0, λ b. b < a) ↔ x0[m] < a, ¬(m + 1 < count(x0, λ b. b < a) ↔ x0[m] < a), x0 ≠ [], m < # x0, ordered≤(a0 ' + x0), ¬ a0 < a ⊦

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 ⊦ n + 0 = n; (s)

Proof step 14 from proof ordered-count-splits (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 15:

  m < count(x0, λ b. b < a) ↔ x0[m] < a, ¬(m + 1 < count(x0, λ b. b < a) ↔ x0[m] < a), x0 ≠ [], m < # x0, m < count(x0, λ b. b < a), ordered≤(a0 ' + x0), ¬ a0 < a ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ m < n → ¬ m + m0 < n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used formulas: m < count(x0, λ b. b < a)

Proof step 15 from proof ordered-count-splits (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  count(x0, λ b. b < a) = m + 1, x0 ≠ [], x0[m] < a, m < # x0, ordered≤(a0 ' + x0), ¬ a0 < a ⊦

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 + 1 ≤ n ↔ m < n; (s) ⊦ ¬ n < n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); (s) ⊦ m + 1 ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 16 from proof ordered-count-splits (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ b < a ∧ b ∈ x → ¬ ordered≤(a ' + x)

Rule argument

Additional information

Used simplifier rules: ⊦ m < # x → (x[m] ∈ x ↔ true); (ss) nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification weakord[tord] leq-trans: ⊦ ¬ b < a ∧ ¬ c < b → ¬ c < a; (forward) from specification weakord[tord] Used terms: a0, x0, x0[m]

Proof step 17 from proof ordered-count-splits (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof ordered-count-splits (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  count(x0, λ b. b < a) ≠ 0, ordered≤(a0 ' + x0), ¬ a0 < a, ∀ n0, a1. (n0 < count(x0, λ b. b < a1) ↔ x0[n0] < a1) ∨ x0 = [] ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ m; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≠ 0; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ a '[0] = a; (s) ⊦ n + 0 = n; (s) ⊦ ¬ a < a; (s) nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ m < 1 ↔ m = 0; (s) ⊦ # a ' = 0 +1; (s)

Proof step 19 from proof ordered-count-splits (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 20:

  count(x0, λ b. b < a) ≠ 0, x0 ≠ [], ordered≤(a0 ' + x0), ¬ a0 < a, ∀ n0, a1. (n0 < count(x0, λ b. b < a1) ↔ x0[n0] < a1) ∨ x0 = [] ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ count([], p) = 0; (s) Used formulas: x0 = []

Proof step 20 from proof ordered-count-splits (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  count(x0, λ b. b < a) ≠ 0, x0 ≠ [], ordered≤(a0 ' + x0), ¬ a0 < a, ∀ n0, a1. (n0 < count(x0, λ b. b < a1) ↔ x0[n0] < a1) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Proof step 21 from proof ordered-count-splits (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ count(x, p) = 0 ↔ (∀ n. n < # x → ¬ p(x[n]))

• Proof step 23:

  x0 ≠ [], ordered≤(a0 ' + x0), ¬ a0 < a, ∀ n0, a1. (n0 < count(x0, λ b. b < a1) ↔ x0[n0] < a1) ∨ ¬ n0 < # x0, ∃ n. ¬(n < # x0 → ¬ x0[n] < a) ⊦

Rule argument

Additional information

Used terms: x0, λ b. b < a

Proof step 22 from proof ordered-count-splits (previous step) (back to tree)

A spec-lemma

Proof step 23 from proof ordered-count-splits (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  x0 ≠ [], n < # x0, x0[n] < a, ordered≤(a0 ' + x0), ¬ a0 < a, ∀ n0, a1. (n0 < count(x0, λ b. b < a1) ↔ x0[n0] < a1) ∨ ¬ n0 < # x0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 24 from proof ordered-count-splits (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ b < a ∧ b ∈ x → ¬ ordered≤(a ' + x)

Rule argument

Additional information

Used simplifier rules: ⊦ m < # x → (x[m] ∈ x ↔ true); (ss) nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification weakord[tord] leq-trans: ⊦ ¬ b < a ∧ ¬ c < b → ¬ c < a; (forward) from specification weakord[tord] Used terms: a0, x0, x0[n]

Proof step 25 from proof ordered-count-splits (previous step) (back to tree)

A spec-lemma