Proof step 1 from proof count0-leq-clean0-ind (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  count(mx[c]c, 0, m, λ j. j < i) ≠ m, c < #c mx, m ≤ #clean0rows(mx, i) ⊦

Rule argument

Additional information

Proof step 2 from proof count0-leq-clean0-ind (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  count(mx[c]c, 0, m0 +1, λ j. j < i) ≠ m0 +1, c < #c mx, m0 +1 ≤ #clean0rows(mx, i), ∀ mx, c, i. ¬(count(mx[c]c, 0, m0, λ j. j < i) ≠ m0 ∧ c < #c mx ∧ m0 ≤ #clean0rows(mx, i)) ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; ⊦ # mx[c]c = #r mx; (s) ⊦ 0 ≤ m; (s) m ≤ # x ⊦ count(x, m, m, p) = 0; (s)

Proof step 3 from proof count0-leq-clean0-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  count(mx[c]c, 0, m0, λ j. j < i) + (mx[m0, c] < i ⊃ 1;0) ≠ m0 + 1, m0 < #clean0rows(mx, i), c < #c mx, ∀ mx0, c0, i0. count(mx0[c0]c, 0, m0, λ j. j < i0) = m0 ∨ ¬ c0 < #c mx0 ∨ ¬ m0 ≤ #clean0rows(mx0, i0) ⊦

Rule argument

Additional information

Used simplifier rules: clean0rows-bounded: ⊦ ¬ #r mx < #clean0rows(mx, i); ⊦ m < n → n ≠ 0; (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 = m + 1; (s) ⊦ mx[c]c[r] = mx[r, c]; (s) m ≤ n, n ≤ # x ⊦ count(x, m, n + 1, p) = count(x, m, n, p) + (p(x[n]) ⊃ 1;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 ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ # mx[c]c = #r mx; (s) ⊦ 0 ≤ m; (s)

Proof step 4 from proof count0-leq-clean0-ind (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

  count(mx[c]c, 0, m0, λ j. j < i) + 1 ≠ m0 + 1, c < #c mx, m0 < #clean0rows(mx, i), mx[m0, c] < i, ∀ mx0, c0, i0. count(mx0[c0]c, 0, m0, λ j. j < i0) = m0 ∨ ¬ c0 < #c mx0 ∨ ¬ m0 ≤ #clean0rows(mx0, i0) ⊦

• Proof step 7:

  count(mx[c]c, 0, m0, λ j. j < i) + 0 ≠ m0 + 1, c < #c mx, m0 < #clean0rows(mx, i), ¬ mx[m0, c] < i, ∀ mx0, c0, i0. count(mx0[c0]c, 0, m0, λ j. j < i0) = m0 ∨ ¬ c0 < #c mx0 ∨ ¬ m0 ≤ #clean0rows(mx0, i0) ⊦

Rule argument

Additional information

Proof step 5 from proof count0-leq-clean0-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  count(mx[c]c, 0, m0, λ j. j < i) ≠ m0, mx[m0, c] < i, m0 < #clean0rows(mx, i), c < #c mx, ∀ mx0, c0, i0. count(mx0[c0]c, 0, m0, λ j. j < i0) = m0 ∨ ¬ c0 < #c mx0 ∨ ¬ m0 ≤ #clean0rows(mx0, i0) ⊦

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)

Proof step 6 from proof count0-leq-clean0-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: mx, c, i

Proof step 7 from proof count0-leq-clean0-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  count(mx[c]c, 0, m0, λ j. j < i) ≠ m0 + 1, m0 < #clean0rows(mx, i), c < #c mx, ¬ mx[m0, c] < i, ∀ mx0, c0, i0. count(mx0[c0]c, 0, m0, λ j. j < i0) = m0 ∨ ¬ c0 < #c mx0 ∨ ¬ m0 ≤ #clean0rows(mx0, i0) ⊦

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 8 from proof count0-leq-clean0-ind (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 9:

  ⊦ ¬ #r mx < #clean0rows(mx, i)

• Proof step 10:

  count(mx[c]c, 0, m0, λ j. j < i) ≠ m0 + 1, c < #c mx, m0 < #clean0rows(mx, i), ¬ #r mx < #clean0rows(mx, i), ¬ mx[m0, c] < i, ∀ mx0, c0, i0. count(mx0[c0]c, 0, m0, λ j. j < i0) = m0 ∨ ¬ c0 < #c mx0 ∨ ¬ m0 ≤ #clean0rows(mx0, i0) ⊦

Rule argument

Additional information

Used terms: mx, i

Proof step 9 from proof count0-leq-clean0-ind (previous step) (back to tree)

Lemma clean0rows-bounded

Proof step 10 from proof count0-leq-clean0-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  count(mx[c]c, 0, m0, λ j. j < i) ≠ m0 + 1, m0 < #clean0rows(mx, i), c < #c mx, m0 < #r mx, #clean0rows(mx, i) ≤ #r mx, ¬ mx[m0, c] < i, ∀ mx0, c0, i0. count(mx0[c0]c, 0, m0, λ j. j < i0) = m0 ∨ ¬ c0 < #c mx0 ∨ ¬ m0 ≤ #clean0rows(mx0, i0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 11 from proof count0-leq-clean0-ind (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 12:

  ⊦ r < #clean0rows(mx, i) → count(mx[r]r, λ j. ¬ j < i) = 0

• Proof step 13:

  count(mx[c]c, 0, m0, λ j. j < i) ≠ m0 + 1, m0 < #r mx, c < #c mx, m0 < #clean0rows(mx, i), #clean0rows(mx, i) ≤ #r mx, ¬ mx[m0, c] < i, m0 < #clean0rows(mx, i) → count(mx[m0]r, λ j. ¬ j < i) = 0, ∀ mx0, c0, i0. count(mx0[c0]c, 0, m0, λ j. j < i0) = m0 ∨ ¬ c0 < #c mx0 ∨ ¬ m0 ≤ #clean0rows(mx0, i0) ⊦

Rule argument

Additional information

Used terms: m0, mx, i

Proof step 12 from proof count0-leq-clean0-ind (previous step) (back to tree)

Lemma clean0rows-allls

Proof step 13 from proof count0-leq-clean0-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  count(mx[m0]r, λ j. ¬ j < i) = 0, count(mx[c]c, 0, m0, λ j. j < i) ≠ m0 + 1, m0 < #clean0rows(mx, i), c < #c mx, m0 < #r mx, #clean0rows(mx, i) ≤ #r mx, ¬ mx[m0, c] < i, ∀ mx0, c0, i0. count(mx0[c0]c, 0, m0, λ j. j < i0) = m0 ∨ ¬ c0 < #c mx0 ∨ ¬ m0 ≤ #clean0rows(mx0, i0) ⊦

Rule argument

Additional information

Proof step 14 from proof count0-leq-clean0-ind (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  count(mx[c]c, 0, m0, λ j. j < i) ≠ m0 + 1, m0 < #r mx, c < #c mx, m0 < #clean0rows(mx, i), #clean0rows(mx, i) ≤ #r mx, ¬ mx[m0, c] < i, ∀ mx0, c0, i0. count(mx0[c0]c, 0, m0, λ j. j < i0) = m0 ∨ ¬ c0 < #c mx0 ∨ ¬ m0 ≤ #clean0rows(mx0, i0), ∀ n. n < # mx[m0]r → ¬ ¬ mx[m0]r[n] < i ⊦

Rule argument

Additional information

Used terms: mx[m0]r, λ j. ¬ j < i

Proof step 15 from proof count0-leq-clean0-ind (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof count0-leq-clean0-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  count(mx[c]c, 0, m0, λ j. j < i) ≠ m0 + 1, m0 < #clean0rows(mx, i), c < #c mx, m0 < #r mx, #clean0rows(mx, i) ≤ #r mx, ¬ mx[m0, c] < i, ∀ mx0, c0, i0. count(mx0[c0]c, 0, m0, λ j. j < i0) = m0 ∨ ¬ c0 < #c mx0 ∨ ¬ m0 ≤ #clean0rows(mx0, i0), ∀ n. n < #c mx → mx[m0, n] < i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mx[r]r[c] = mx[r, c]; (s) ⊦ # mx[r]r = #c mx; (s)

Proof step 17 from proof count0-leq-clean0-ind (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: c