Proof step 1 from proof countodd-zero-ind (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  countodd(a, m, n, p) ≠ 0, n ≤ # a, m ≤ n, ∀ r. m ≤ r ∧ r < n ∧ odd(r) → ¬ p(a[r]) ⊦

Rule argument

Additional information

Proof step 2 from proof countodd-zero-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  countodd(a, m, n, p) ≠ 0, m ≤ n, n ≤ # a, m ≤ # a, ∀ r. m ≤ r ∧ r < n ∧ odd(r) → ¬ p(a[r]) ⊦

Rule argument

Additional information

Used simplifier rules: let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat

Proof step 3 from proof countodd-zero-ind (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  countodd(a, m, n0 +1, p) ≠ 0, m ≤ # a, n0 +1 ≤ # a, m ≤ n0 +1, ∀ r. m ≤ r ∧ r < n0 +1 ∧ odd(r) → ¬ p(a[r]), ∀ a, m, p. ¬(countodd(a, m, n0, p) ≠ 0 ∧ m ≤ n0 ∧ n0 ≤ # a ∧ m ≤ # a ∧ (∀ r. m ≤ r ∧ r < n0 ∧ odd(r) → ¬ p(a[r]))) ⊦

Rule argument

Additional information

Used simplifier rules: countodd-base: m ≤ # a ⊦ countodd(a, m, m, p) = 0; nat freely generated by 0, +1;; ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ ¬ n < 0; (s) ⊦ 0 ≤ m; (s)

Proof step 4 from proof countodd-zero-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

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 < n + 1 ↔ ¬ n < m; (s) ⊦ m +1 = m + 1; (s) ⊦ m + 1 ≤ n ↔ m < n; (s)

Proof step 5 from proof countodd-zero-ind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  a ≠ [], countodd(a, m, n0 + 1, p) ≠ 0, n0 < # a, m ≤ # a, m ≤ n0 + 1, ∀ r. m ≤ r ∧ ¬ n0 < r ∧ odd(r) → ¬ p(a[r]), countodd(a, m, n0, p) = 0 ∨ ¬ m ≤ n0 ∨ ¬ n0 ≤ # a ∨ ¬ m ≤ # a ∨ ¬(∀ r. m ≤ r ∧ r < n0 ∧ odd(r) → ¬ p(a[r])) ⊦

Rule argument

Additional information

Used terms: a, m, p

Proof step 6 from proof countodd-zero-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  a ≠ [], countodd(a, m, n0 + 1, p) ≠ 0, n0 < # a, m ≤ n0 + 1, m ≤ # a, ∀ r. m ≤ r ∧ ¬ n0 < r ∧ odd(r) → ¬ p(a[r]), countodd(a, m, n0, p) = 0 ∨ ¬ m ≤ n0 ∨ ¬(m ≤ r ∧ r < n0 ∧ odd(r) → ¬ p(a[r])) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s)

Proof step 7 from proof countodd-zero-ind (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

  countodd(a, m, n0, p) + (odd(n0) ∧ p(a[n0]) ⊃ 1;0) ≠ 0, a ≠ [], n0 < # a, m ≤ # a, m ≤ n0 + 1, m ≤ n0, n0 ≤ # a, ∀ r. m ≤ r ∧ ¬ n0 < r ∧ odd(r) → ¬ p(a[r]), countodd(a, m, n0, p) = 0 ∨ ¬ m ≤ n0 ∨ ¬(m ≤ r ∧ r < n0 ∧ odd(r) → ¬ p(a[r])) ⊦

Rule argument

Additional information

Used simplifier rules: 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 Used terms: a, m, n0, p

Proof step 8 from proof countodd-zero-ind (previous step) (back to tree)

Lemma countodd-rec

Proof step 9 from proof countodd-zero-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  countodd(a, m, n0, p) + (odd(n0) ∧ p(a[n0]) ⊃ 1;0) ≠ 0, a ≠ [], m < # a, n0 < # a, m ≤ n0 + 1, m ≤ n0, ∀ r. m ≤ r ∧ ¬ n0 < r ∧ odd(r) → ¬ p(a[r]), countodd(a, m, n0, p) = 0 ∨ ¬(m ≤ r ∧ r < n0 ∧ odd(r) → ¬ p(a[r])) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat

Proof step 10 from proof countodd-zero-ind (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  countodd(a, m, n0, p) = 0, countodd(a, m, n0, p) + (odd(n0) ∧ p(a[n0]) ⊃ 1;0) ≠ 0, a ≠ [], n0 < # a, m < # a, m ≤ n0, m ≤ n0 + 1, ∀ r. m ≤ r ∧ ¬ n0 < r ∧ odd(r) → ¬ p(a[r]) ⊦

• Proof step 13:

  countodd(a, m, n0, p) + (odd(n0) ∧ p(a[n0]) ⊃ 1;0) ≠ 0, a ≠ [], r < n0, n0 < # a, m < # a, odd(r), p(a[r]), m ≤ r, m ≤ n0, m ≤ n0 + 1, ∀ r. m ≤ r ∧ ¬ n0 < r ∧ odd(r) → ¬ p(a[r]) ⊦

Rule argument

Additional information

Proof step 11 from proof countodd-zero-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  countodd(a, m, n0, p) = 0, a ≠ [], m < # a, n0 < # a, odd(n0), p(a[n0]), m ≤ n0 + 1, m ≤ n0, ∀ r. m ≤ r ∧ ¬ n0 < r ∧ odd(r) → ¬ p(a[r]) ⊦

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 = 0 ↔ m = 0 ∧ n = 0; (ws)

Proof step 12 from proof countodd-zero-ind (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < n; (s) Used terms: n0

Proof step 13 from proof countodd-zero-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  countodd(a, m, n0, p) + (odd(n0) ∧ p(a[n0]) ⊃ 1;0) ≠ 0, a ≠ [], r + 1 < # a, m < # a, n0 < # a, r < n0, m < n0, r < # a, m + 1 < # a, odd(r), p(a[r]), m ≤ n0 + 1, m ≤ r, ∀ r. m ≤ r ∧ ¬ n0 < r ∧ odd(r) → ¬ p(a[r]) ⊦

Rule argument

Additional information

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

Proof step 14 from proof countodd-zero-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 → ¬ n < m; (s) Used terms: r