Proof step 1 from proof count-add-even-odd-ind (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  countevn(a, m, n, p) + countodd(a, m, n, p) ≠ count(a, m, n, p), n ≤ # a, m ≤ n ⊦

Rule argument

Additional information

Proof step 2 from proof count-add-even-odd-ind (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  countevn(a, m, n0 +1, p) + countodd(a, m, n0 +1, p) ≠ count(a, m, n0 +1, p), m ≤ n0 +1, n0 +1 ≤ # a, ∀ a, m, p. ¬(countevn(a, m, n0, p) + countodd(a, m, n0, p) ≠ count(a, m, n0, p) ∧ n0 ≤ # a ∧ m ≤ n0) ⊦

Rule argument

Additional information

Used simplifier rules: countevn-base: m ≤ # a ⊦ countevn(a, m, m, p) = 0; countodd-base: m ≤ # a ⊦ countodd(a, m, m, p) = 0; nat freely generated by 0, +1;; ⊦ m ≤ 0 ↔ m = 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ 0 ≤ m; (s) m ≤ # x ⊦ count(x, m, m, p) = 0; (s)

Proof step 3 from proof count-add-even-odd-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  countevn(a, m, n0 + 1, p) + countodd(a, m, n0 + 1, p) ≠ count(a, m, n0 + 1, p), a ≠ [], n0 < # a, m ≤ # a, m ≤ n0 + 1, ∀ a0, m0, p0. countevn(a0, m0, n0, p0) + countodd(a0, m0, n0, p0) = count(a0, m0, n0, p0) ∨ ¬ n0 ≤ # a0 ∨ ¬ m0 ≤ n0 ⊦

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 le-one: ⊦ m ≤ n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat ⊦ m +1 = m + 1; (s) ⊦ m + 1 ≤ n ↔ m < n; (s)

Proof step 4 from proof count-add-even-odd-ind (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  m ≤ n, n ≤ # a ⊦ countevn(a, m, n + 1, p) = countevn(a, m, n, p) + (even(n) ∧ p(a[n]) ⊃ 1;0)

• Proof step 6:

  (countevn(a, m, n0, p) + (even(n0) ∧ p(a[n0]) ⊃ 1;0)) + countodd(a, m, n0 + 1, p) ≠ count(a, m, n0 + 1, p), a ≠ [], n0 < # a, m ≤ n0 + 1, m ≤ # a, m ≤ n0, n0 ≤ # a, ∀ a0, m0, p0. countevn(a0, m0, n0, p0) + countodd(a0, m0, n0, p0) = count(a0, m0, n0, p0) ∨ ¬ n0 ≤ # a0 ∨ ¬ m0 ≤ n0 ⊦

Rule argument

Additional information

Used simplifier rules: countevn-base: m ≤ # a ⊦ countevn(a, m, m, p) = 0; countodd-base: m ≤ # a ⊦ countodd(a, m, m, p) = 0; ⊦ m < n → m ≤ n; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m + 1 ≠ 0; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic m ≤ # x ⊦ count(x, m, m, p) = 0; (s) Used terms: a, m, n0, p

Proof step 5 from proof count-add-even-odd-ind (previous step) (back to tree)

Lemma countevn-rec

Proof step 6 from proof count-add-even-odd-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  countevn(a, m, n0, p) + (even(n0) ∧ p(a[n0]) ⊃ 1;0) + countodd(a, m, n0, p) + (odd(n0) ∧ p(a[n0]) ⊃ 1;0) ≠ count(a, m, n0, p) + (p(a[n0]) ⊃ 1;0), a ≠ [], m < # a, n0 < # a, m ≤ n0 + 1, m ≤ n0, ∀ a0, m0, p0. countevn(a0, m0, n0, p0) + countodd(a0, m0, n0, p0) = count(a0, m0, n0, p0) ∨ ¬ n0 ≤ # a0 ∨ ¬ m0 ≤ n0 ⊦

Rule argument

Additional information

Used simplifier rules: countodd-rec: m ≤ n, n ≤ # a ⊦ countodd(a, m, n + 1, p) = countodd(a, m, n, p) + (odd(n) ∧ p(a[n]) ⊃ 1;0); ⊦ m < n → m ≤ n; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic m ≤ n, n ≤ # x ⊦ count(x, m, n + 1, p) = count(x, m, n, p) + (p(x[n]) ⊃ 1;0); (s)

Proof step 7 from proof count-add-even-odd-ind (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 8:

  countevn(a, m, n0, p) + 1 + countodd(a, m, n0, p) + (odd(n0) ∧ p(a[n0]) ⊃ 1;0) ≠ count(a, m, n0, p) + (p(a[n0]) ⊃ 1;0), a ≠ [], n0 < # a, m < # a, even(n0), p(a[n0]), m ≤ n0, m ≤ n0 + 1, ∀ a0, m0, p0. countevn(a0, m0, n0, p0) + countodd(a0, m0, n0, p0) = count(a0, m0, n0, p0) ∨ ¬ n0 ≤ # a0 ∨ ¬ m0 ≤ n0 ⊦

• Proof step 10:

  countevn(a, m, n0, p) + 0 + countodd(a, m, n0, p) + (odd(n0) ∧ p(a[n0]) ⊃ 1;0) ≠ count(a, m, n0, p) + (p(a[n0]) ⊃ 1;0), a ≠ [], n0 < # a, m < # a, m ≤ n0, m ≤ n0 + 1, ∀ a0, m0, p0. countevn(a0, m0, n0, p0) + countodd(a0, m0, n0, p0) = count(a0, m0, n0, p0) ∨ ¬ n0 ≤ # a0 ∨ ¬ m0 ≤ n0, ¬ even(n0) ∨ ¬ p(a[n0]) ⊦

Rule argument

Additional information

Proof step 8 from proof count-add-even-odd-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  countevn(a, m, n0, p) + countodd(a, m, n0, p) ≠ count(a, m, n0, p), a ≠ [], m < # a, n0 < # a, even(n0), p(a[n0]), m ≤ n0 + 1, m ≤ n0, ∀ a0, m0, p0. countevn(a0, m0, n0, p0) + countodd(a0, m0, n0, p0) = count(a0, m0, n0, p0) ∨ ¬ n0 ≤ # a0 ∨ ¬ m0 ≤ 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 + n0 ↔ n = n0; (s) ⊦ even(n) → ¬ odd(n); (s)

Proof step 9 from proof count-add-even-odd-ind (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: a, m, p

Proof step 10 from proof count-add-even-odd-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  countevn(a, m, n0, p) + countodd(a, m, n0, p) + (odd(n0) ∧ p(a[n0]) ⊃ 1;0) ≠ count(a, m, n0, p) + (p(a[n0]) ⊃ 1;0), a ≠ [], m < # a, n0 < # a, m ≤ n0 + 1, m ≤ n0, ∀ a0, m0, p0. countevn(a0, m0, n0, p0) + countodd(a0, m0, n0, p0) = count(a0, m0, n0, p0) ∨ ¬ n0 ≤ # a0 ∨ ¬ m0 ≤ n0, ¬ even(n0) ∨ ¬ p(a[n0]) ⊦

Rule argument

Additional information

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

Proof step 11 from proof count-add-even-odd-ind (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 12:

  countevn(a, m, n0, p) + countodd(a, m, n0, p) + 1 ≠ count(a, m, n0, p) + (p(a[n0]) ⊃ 1;0), a ≠ [], n0 < # a, m < # a, odd(n0), p(a[n0]), m ≤ n0, m ≤ n0 + 1, ∀ a0, m0, p0. countevn(a0, m0, n0, p0) + countodd(a0, m0, n0, p0) = count(a0, m0, n0, p0) ∨ ¬ n0 ≤ # a0 ∨ ¬ m0 ≤ n0, ¬ even(n0) ∨ ¬ p(a[n0]) ⊦

• Proof step 14:

  countevn(a, m, n0, p) + countodd(a, m, n0, p) + 0 ≠ count(a, m, n0, p) + (p(a[n0]) ⊃ 1;0), a ≠ [], n0 < # a, m < # a, m ≤ n0, m ≤ n0 + 1, ∀ a0, m0, p0. countevn(a0, m0, n0, p0) + countodd(a0, m0, n0, p0) = count(a0, m0, n0, p0) ∨ ¬ n0 ≤ # a0 ∨ ¬ m0 ≤ n0, ¬ even(n0) ∨ ¬ p(a[n0]), ¬ odd(n0) ∨ ¬ p(a[n0]) ⊦

Rule argument

Additional information

Proof step 12 from proof count-add-even-odd-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  countevn(a, m, n0, p) + countodd(a, m, n0, p) ≠ count(a, m, n0, p), a ≠ [], m < # a, n0 < # a, odd(n0), p(a[n0]), m ≤ n0 + 1, m ≤ n0, ∀ a0, m0, p0. countevn(a0, m0, n0, p0) + countodd(a0, m0, n0, p0) = count(a0, m0, n0, p0) ∨ ¬ n0 ≤ # a0 ∨ ¬ m0 ≤ n0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ odd(n) → ¬ even(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 + n0 ↔ n = n0; (s)

Proof step 13 from proof count-add-even-odd-ind (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: a, m, p

Proof step 14 from proof count-add-even-odd-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  countevn(a, m, n0, p) + countodd(a, m, n0, p) ≠ count(a, m, n0, p) + (p(a[n0]) ⊃ 1;0), a ≠ [], m < # a, n0 < # a, m ≤ n0 + 1, m ≤ n0, ∀ a0, m0, p0. countevn(a0, m0, n0, p0) + countodd(a0, m0, n0, p0) = count(a0, m0, n0, p0) ∨ ¬ n0 ≤ # a0 ∨ ¬ m0 ≤ n0, ¬ odd(n0) ∨ ¬ p(a[n0]), ¬ even(n0) ∨ ¬ p(a[n0]) ⊦

Rule argument

Additional information

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

Proof step 15 from proof count-add-even-odd-ind (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 16:

  countevn(a, m, n0, p) + countodd(a, m, n0, p) ≠ count(a, m, n0, p) + (p(a[n0]) ⊃ 1;0), a ≠ [], n0 < # a, m < # a, m ≤ n0, m ≤ n0 + 1, ¬ p(a[n0]), ∀ a0, m0, p0. countevn(a0, m0, n0, p0) + countodd(a0, m0, n0, p0) = count(a0, m0, n0, p0) ∨ ¬ n0 ≤ # a0 ∨ ¬ m0 ≤ n0, ¬ even(n0) ∨ ¬ p(a[n0]), ¬ odd(n0) ∨ ¬ p(a[n0]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ odd(n) ↔ ¬ even(n); (ss) Used formulas: p(a[n0])

Proof step 16 from proof count-add-even-odd-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  countevn(a, m, n0, p) + countodd(a, m, n0, p) ≠ count(a, m, n0, p), a ≠ [], m < # a, n0 < # a, m ≤ n0 + 1, m ≤ n0, ¬ p(a[n0]), ∀ a0, m0, p0. countevn(a0, m0, n0, p0) + countodd(a0, m0, n0, p0) = count(a0, m0, n0, p0) ∨ ¬ n0 ≤ # a0 ∨ ¬ m0 ≤ 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 ⊦ n + 0 = n; (s)

Proof step 17 from proof count-add-even-odd-ind (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: a, m, p