Proof step 1 from proof countevn-maxcol0-bounded (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  c0 < #c mx0, ¬ countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2 ⊦

Rule argument

Additional information

Proof step 2 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c0 < #c mx0 ⊦

Rule argument

Additional information

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

Proof step 3 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx

• Proof step 5:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, c0 < #c mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: mx0, i

Proof step 4 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Lemma dirtyrows-def

Proof step 5 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  m ≤ n, n ≤ n0, n0 ≤ # a ⊦ countevn(a, m, n, p) + countevn(a, n, n0, p) = countevn(a, m, n0, p)

• Proof step 7:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0 - #clean1rows(mx0, i), λ j. j < i) + countevn(mx0[c0]c, #r mx0 - #clean1rows(mx0, i), #r mx0, λ j. j < i), c0 < #c mx0, #clean0rows(mx0, i) ≤ #r mx0 - #clean1rows(mx0, i), #r mx0 - #clean1rows(mx0, i) ≤ #r mx0, #r mx0 ≤ # mx0[c0]c ⊦

Rule argument

Additional information

Used simplifier rules: clean1rows-bounded: ⊦ ¬ #r mx < #clean1rows(mx, i); clean0-plus-clean1-bounded: #c mx ≠ 0 ⊦ ¬ #r mx < #clean0rows(mx, i) + #clean1rows(mx, i); n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s) n0 ≤ n ⊦ n - n0 ≤ m ↔ n ≤ m + n0; (s) ⊦ m ≤ m + n; (s) ⊦ # mx[c]c = #r mx; (s) ⊦ m ≤ m; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → n ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: #r mx0, λ j. j < i, mx0[c0]c, #r mx0 - #clean1rows(mx0, i), #clean0rows(mx0, i)

Proof step 6 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Lemma countevn-append-ind

Proof step 7 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ∀ r. m ≤ r ∧ r < n ∧ even(r) → ¬ p(a[r]), m ≤ n, n ≤ # a ⊦ countevn(a, m, n, p) = 0

• Proof step 9:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, c0 < #c mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0 - #clean1rows(mx0, i), λ j. j < i) + countevn(mx0[c0]c, #r mx0 - #clean1rows(mx0, i), #r mx0, λ j. j < i), #r mx0 ≤ # mx0[c0]c, #r mx0 - #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #r mx0 - #clean1rows(mx0, i) ⊦ (∀ r. #r mx0 - #clean1rows(mx0, i) ≤ r ∧ r < #r mx0 ∧ even(r) → ¬ mx0[c0]c[r] < i) ∧ #r mx0 - #clean1rows(mx0, i) ≤ #r mx0 ∧ #r mx0 ≤ # mx0[c0]c

• Proof step 17:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, c0 < #c mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0 - #clean1rows(mx0, i), λ j. j < i) + 0, #clean0rows(mx0, i) ≤ #r mx0 - #clean1rows(mx0, i), #r mx0 - #clean1rows(mx0, i) ≤ #r mx0, #r mx0 ≤ # mx0[c0]c, ∀ r. #r mx0 - #clean1rows(mx0, i) ≤ r ∧ r < #r mx0 ∧ even(r) → ¬ mx0[c0]c[r] < i ⊦

Rule argument

Additional information

Used terms: mx0[c0]c, #r mx0 - #clean1rows(mx0, i), #r mx0, λ j. j < i

Proof step 8 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Lemma countevn-zero-ind

Proof step 9 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #clean1rows(mx0, i) ≠ 0, #dirtyrows(mx0, i) + #clean1rows(mx0, i) ≠ 0, #clean0rows(mx0, i) < #r mx0, c0 < #c mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), mx0[r, c0] < i, r < #r mx0, #clean0rows(mx0, i) < r + #clean1rows(mx0, i), even(r), #clean0rows(mx0, i) ≤ r, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #r mx0 ≤ r + #clean1rows(mx0, i) ⊦

Rule argument

Additional information

Used simplifier rules: countevn-append-ind: m ≤ n, n ≤ n0, n0 ≤ # a ⊦ countevn(a, m, n, p) + countevn(a, n, n0, p) = countevn(a, m, n0, p); clean1rows-bounded: ⊦ ¬ #r mx < #clean1rows(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 < m + n ↔ n ≠ 0; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m ≤ m; (s) ⊦ # mx[c]c = #r mx; (s) ⊦ m ≤ m + n; (s) n0 ≤ n ⊦ n - n0 ≤ m ↔ n ≤ m + n0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ mx[c]c[r] = mx[r, c]; (s) n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s)

Proof step 10 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 11:

  ⊦ #r mx ≤ #clean1rows(mx, i) + r ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0

• Proof step 12:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #clean1rows(mx0, i) ≠ 0, #dirtyrows(mx0, i) + #clean1rows(mx0, i) ≠ 0, #clean0rows(mx0, i) < r + #clean1rows(mx0, i), r < #r mx0, mx0[r, c0] < i, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c0 < #c mx0, #clean0rows(mx0, i) < #r mx0, even(r), #r mx0 ≤ r + #clean1rows(mx0, i), #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ r, #r mx0 ≤ #clean1rows(mx0, i) + r ∧ r < #r mx0 → count(mx0[r]r, λ j. j < i) = 0 ⊦

Rule argument

Additional information

Used terms: mx0, i, r

Proof step 11 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Lemma clean1rows-allge

Proof step 12 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, count(mx0[r]r, λ j. j < i) = 0, #clean1rows(mx0, i) ≠ 0, #dirtyrows(mx0, i) + #clean1rows(mx0, i) ≠ 0, #clean0rows(mx0, i) < #r mx0, c0 < #c mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), mx0[r, c0] < i, r < #r mx0, #clean0rows(mx0, i) < r + #clean1rows(mx0, i), even(r), #clean0rows(mx0, i) ≤ r, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #r mx0 ≤ r + #clean1rows(mx0, i) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic

Proof step 13 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #clean1rows(mx0, i) ≠ 0, #dirtyrows(mx0, i) + #clean1rows(mx0, i) ≠ 0, #clean0rows(mx0, i) < r + #clean1rows(mx0, i), r < #r mx0, mx0[r, c0] < i, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c0 < #c mx0, #clean0rows(mx0, i) < #r mx0, even(r), #r mx0 ≤ r + #clean1rows(mx0, i), #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ r, ∀ n. n < # mx0[r]r → ¬ mx0[r]r[n] < i ⊦

Rule argument

Additional information

Used terms: mx0[r]r, λ j. j < i

Proof step 14 from proof countevn-maxcol0-bounded (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #clean1rows(mx0, i) ≠ 0, #dirtyrows(mx0, i) + #clean1rows(mx0, i) ≠ 0, #clean0rows(mx0, i) < #r mx0, c0 < #c mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), mx0[r, c0] < i, r < #r mx0, #clean0rows(mx0, i) < r + #clean1rows(mx0, i), even(r), #clean0rows(mx0, i) ≤ r, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #r mx0 ≤ r + #clean1rows(mx0, i), ∀ n. n < #c mx0 → ¬ mx0[r, 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 16 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: c0

Proof step 17 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0 - #clean1rows(mx0, i), λ j. j < i), c0 < #c mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: clean1rows-bounded: ⊦ ¬ #r mx < #clean1rows(mx, i); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ mx[c]c[r] = mx[r, c]; (s) n0 ≤ n ⊦ n - n0 ≤ m ↔ n ≤ m + n0; (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 ⊦ n + 0 = n; (s) n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s) ⊦ m ≤ m + n; (s) ⊦ m ≤ m; (s) ⊦ # mx[c]c = #r mx; (s)

Proof step 18 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 19:

  #r mx0 = n0 + #clean1rows(mx0, i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, c0 < #c mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), n0, λ j. j < i), #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: clean1rows-bounded: ⊦ ¬ #r mx < #clean1rows(mx, i); ⊦ m ≤ n ↔ ¬ n < m; (ss) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: #r mx0, #clean1rows(mx0, i), n0

Proof step 19 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), c0 < #c mx0, #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 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 eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic

Proof step 20 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 21:

  m ≤ n, n ≤ # a ⊦ countevn(a, m, n, p) ≤ (even(m) ⊃ (n + 1 - m) / 2;(n - m) / 2)

• Proof step 22:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, c0 < #c mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) ≤ (even(#clean0rows(mx0, i)) ⊃ ((#clean0rows(mx0, i) + #dirtyrows(mx0, i)) + 1 - #clean0rows(mx0, i)) / 2 ;(#clean0rows(mx0, i) + #dirtyrows(mx0, i) - #clean0rows(mx0, i)) / 2 ), ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m + n; (s) ⊦ # mx[c]c = #r mx; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), mx0[c0]c, λ j. j < i

Proof step 21 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Lemma countevn-bounded-ind

Proof step 22 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), c0 < #c mx0, #dirtyrows(mx0, i) /↑ 2 < (even(#clean0rows(mx0, i)) ⊃ (#dirtyrows(mx0, i) + 1) / 2;#dirtyrows(mx0, i) / 2), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) ≤ (even(#clean0rows(mx0, i)) ⊃ (#dirtyrows(mx0, i) + 1) / 2;#dirtyrows(mx0, i) / 2), ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

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 c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n - m = n; (s)

Proof step 23 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 24:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, c0 < #c mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), #dirtyrows(mx0, i) /↑ 2 < (#dirtyrows(mx0, i) + 1) / 2, even(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) ≤ (even(#clean0rows(mx0, i)) ⊃ (#dirtyrows(mx0, i) + 1) / 2;#dirtyrows(mx0, i) / 2), #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

• Proof step 42:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, c0 < #c mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx0, i) / 2, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) ≤ (even(#clean0rows(mx0, i)) ⊃ (#dirtyrows(mx0, i) + 1) / 2;#dirtyrows(mx0, i) / 2), #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, ¬ even(#clean0rows(mx0, i)), ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Proof step 24 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 0, c0 < #c mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), #dirtyrows(mx0, i) /↑ 2 < (#dirtyrows(mx0, i) + 1) / 2, even(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i) + 1, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

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 ⊦ 1 = m + 1 ↔ m = 0; (s) ⊦ m + 1 ≠ 0; (s) ⊦ m / 2 = 0 ↔ m = 0 ∨ m = 1; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic m0 ≠ 0 ⊦ n ≤ m / m0 ↔ n * m0 ≤ m; (s)

Proof step 25 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 26:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) + 1 = m0 * 2 + n0, #dirtyrows(mx0, i) ≠ 0, 2 ≠ 0, #dirtyrows(mx0, i) /↑ 2 < m0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), c0 < #c mx0, n0 < 2, even(#clean0rows(mx0, i)), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i) + 1, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: #dirtyrows(mx0, i) + 1, 2, m0, n0

Proof step 26 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) + 1 = m0 * 2 + n0, #dirtyrows(mx0, i) ≠ 0, #dirtyrows(mx0, i) /↑ 2 < m0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), c0 < #c mx0, n0 < 2, even(#clean0rows(mx0, i)), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ m0 * 2 + n0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 27 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ m /↑ n = (∃ n0. m = n0 * n ⊃ m / n;m / n + 1)

• Proof step 29:

  #dirtyrows(mx0, i) + 1 = m0 * 2 + n0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 0, n0 < 2, c0 < #c mx0, even(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ m0 * 2 + n0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1) < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1) < m0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used terms: #dirtyrows(mx0, i), 2

Proof step 28 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Lemma divup-def

Proof step 29 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 30:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) + 1 = m0 * 2 + n0, #dirtyrows(mx0, i) ≠ 0, c0 < #c mx0, n0 < 2, #dirtyrows(mx0, i) / 2 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), even(#clean0rows(mx0, i)), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ m0 * 2 + n0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1) < m0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2 ⊦

Rule argument

Additional information

Used simplifier rules: f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ n0 < n ∧ n1 < n → (m * n + n0 = m0 * n + n1 ↔ m = m0 ∧ n0 = n1); (ws) ⊦ m < n → n ≠ 0; (s) ⊦ 2 * m = 0 ↔ m = 0; (s) ⊦ (2 * m) / 2 = m; (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ 2 * n ≤ 2 * m + 1 ↔ n ≤ m; (s) ⊦ 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 mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult

Proof step 30 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 31:

  #dirtyrows(mx0, i) = m1 * 2 + n1, #dirtyrows(mx0, i) + 1 = m0 * 2 + n0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 0, 2 ≠ 0, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), n0 < 2, c0 < #c mx0, n1 < 2, even(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ m0 * 2 + n0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: #dirtyrows(mx0, i), 2, m, n

Proof step 31 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  #dirtyrows(mx0, i) = m1 * 2 + n1, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) + 1 = m0 * 2 + n0, #dirtyrows(mx0, i) ≠ 0, n1 < 2, c0 < #c mx0, n0 < 2, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), even(#clean0rows(mx0, i)), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ m0 * 2 + n0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2 ⊦

Rule argument

Additional information

Proof step 32 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 33:

  #dirtyrows(mx0, i) = m1 * 2 + n1, #dirtyrows(mx0, i) + 1 = m0 * 2 + n0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, n0 = 0, #dirtyrows(mx0, i) ≠ 0, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), n0 < 2, c0 < #c mx0, n1 < 2, even(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ m0 * 2 + n0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; ⊦ m + n = m + n0 ↔ n = n0; (s) ⊦ m +1 = m + 1; (s) n < n0 ⊦ m + (* n) < (* n0) ↔ m < n0 - n; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ n + 0 = n; (s) ⊦ 2 * n ≤ 2 * m + 1 ↔ n ≤ m; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ n0 < n → (m * n + n0 = m0 * n ↔ m = m0 ∧ n0 = 0); (ws) ⊦ 2 * m = 0 ↔ m = 0; (s) ⊦ m < n → n ≠ 0; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m + m0 < n → ¬ n + n0 < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 33 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  #dirtyrows(mx0, i) = m1 * 2 + n1, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) + 1 = m0 * 2, #dirtyrows(mx0, i) ≠ 0, n1 < 2, c0 < #c mx0, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), m1 + 1 < m0, even(#clean0rows(mx0, i)), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) ≤ m0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2 ⊦

Rule argument

Additional information

Used simplifier rules: fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult 0 ≠ m ⊦ (* m) * n ≤ m * n0 ↔ n ≤ n0; (s) 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 34 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 35:

  #dirtyrows(mx0, i) = m1 * 2 + n1, #dirtyrows(mx0, i) + 1 = m0 * 2, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, n1 = n2 +1, #dirtyrows(mx0, i) ≠ 0, m1 + 1 < m0, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), c0 < #c mx0, n1 < 2, even(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) ≤ m0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; ⊦ n + 0 = n; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ n0 < n → (m * n + n0 = m0 * n ↔ m = m0 ∧ n0 = 0); (ws) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 35 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  #dirtyrows(mx0, i) = 1 + m1 * 2, #dirtyrows(mx0, i) + 1 = m0 * 2, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 0, m1 + 1 < m0, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), c0 < #c mx0, even(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) ≤ m0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

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 ⊦ m < 1 ↔ m = 0; (s) n < n0 ⊦ m + (* n) < (* n0) ↔ m < n0 - n; (s) ⊦ m +1 = m + 1; (s)

Proof step 36 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 37:

  #dirtyrows(mx0, i) = 1 + m1 * 2, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) + 1 = m0 * 2, m0 = m +1, #dirtyrows(mx0, i) ≠ 0, c0 < #c mx0, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), m1 + 1 < m0, even(#clean0rows(mx0, i)), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) ≤ m0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2 ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 37 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  #dirtyrows(mx0, i) = m1 * 2 + 1, 2 * m = m1 * 2, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 0, c0 < #c mx0, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), m1 < m, even(#clean0rows(mx0, i)), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) ≤ m + 1, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) ≤ m ⊦

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 eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n → n ≠ 0; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m +1 = m + 1; (s) n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n); (s) mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m * (n + 1) = m * n + m; (s)

Proof step 38 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ m * n = n * m

• Proof step 40:

  #dirtyrows(mx0, i) = 2 * m1 + 1, 2 * m = 2 * m1, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 0, m1 < m, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), c0 < #c mx0, even(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) ≤ m + 1, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) ≤ m ⊦

Rule argument

Additional information

Used terms: m1, 2

Proof step 39 from proof countevn-maxcol0-bounded (previous step) (back to tree)

A spec-lemma

Proof step 40 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

  ⊦ m * n = m * n0 ↔ m = 0 ∨ n = n0

Rule argument

Additional information

Used simplifier rules: lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m < n → ¬ n < m; (s) Used terms: 2, m, m1

Proof step 41 from proof countevn-maxcol0-bounded (previous step) (back to tree)

A spec-lemma

Proof step 42 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 0, #dirtyrows(mx0, i) ≠ 1, c0 < #c mx0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx0, i) / 2, odd(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i), #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m / 2 = 0 ↔ m = 0 ∨ m = 1; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ even(n) ↔ ¬ odd(n); (ss) m0 ≠ 0 ⊦ n ≤ m / m0 ↔ n * m0 ≤ m; (s)

Proof step 43 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 44:

  #dirtyrows(mx0, i) = m0 * 2 + n0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 0, #dirtyrows(mx0, i) ≠ 1, 2 ≠ 0, #dirtyrows(mx0, i) /↑ 2 < m0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), c0 < #c mx0, n0 < 2, odd(#clean0rows(mx0, i)), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i), ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: #dirtyrows(mx0, i), 2, m0, n0

Proof step 44 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  #dirtyrows(mx0, i) = m0 * 2 + n0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 1, #dirtyrows(mx0, i) ≠ 0, #dirtyrows(mx0, i) /↑ 2 < m0, #dirtyrows(mx0, i) /↑ 2 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), c0 < #c mx0, n0 < 2, odd(#clean0rows(mx0, i)), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i), ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 45 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 46:

  ⊦ m /↑ n = (∃ n0. m = n0 * n ⊃ m / n;m / n + 1)

• Proof step 47:

  #dirtyrows(mx0, i) = m0 * 2 + n0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 1, #dirtyrows(mx0, i) ≠ 0, n0 < 2, c0 < #c mx0, odd(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i), #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1) < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1) < m0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used terms: #dirtyrows(mx0, i), 2

Proof step 46 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Lemma divup-def

Proof step 47 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 48:

  #dirtyrows(mx0, i) = m0 * 2 + n0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 1, #dirtyrows(mx0, i) ≠ 0, c0 < #c mx0, n0 < 2, #dirtyrows(mx0, i) / 2 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), odd(#clean0rows(mx0, i)), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i), (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1) < m0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2 ⊦

Rule argument

Additional information

Used simplifier rules: f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ n0 < n → (m * n + n0 = m0 * n ↔ m = m0 ∧ n0 = 0); (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ 2 * m = 0 ↔ m = 0; (s) ⊦ 2 * m ≠ 1; (s) ⊦ (2 * m) / 2 = m; (s) 0 ≠ m ⊦ (* m) * n ≤ m * n0 ↔ n ≤ n0; (s) ⊦ m < n → (n ≤ m ↔ false); (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult

Proof step 48 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 49:

  #dirtyrows(mx0, i) = m0 * 2 + n0, #dirtyrows(mx0, i) = m1 * 2 + n1, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 1, #dirtyrows(mx0, i) ≠ 0, 2 ≠ 0, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), n0 < 2, c0 < #c mx0, n1 < 2, odd(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i), #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: #dirtyrows(mx0, i), 2, m, n

Proof step 49 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  #dirtyrows(mx0, i) = m1 * 2 + n1, #dirtyrows(mx0, i) = m0 * 2 + n0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 1, #dirtyrows(mx0, i) ≠ 0, n1 < 2, c0 < #c mx0, n0 < 2, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), odd(#clean0rows(mx0, i)), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i), (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2 ⊦

Rule argument

Additional information

Proof step 50 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 51:

  #dirtyrows(mx0, i) = m0 * 2 + n0, #dirtyrows(mx0, i) = m1 * 2 + n1, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, n0 = n +1, #dirtyrows(mx0, i) ≠ 1, #dirtyrows(mx0, i) ≠ 0, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), n0 < 2, c0 < #c mx0, n1 < 2, odd(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i), #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; ⊦ n + 0 = n; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ n0 < n → (m * n + n0 = m0 * n ↔ m = m0 ∧ n0 = 0); (ws) ⊦ 2 * m = 0 ↔ m = 0; (s) ⊦ 2 * m ≠ 1; (s) 0 ≠ m ⊦ (* m) * n ≤ m * n0 ↔ n ≤ n0; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 51 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  #dirtyrows(mx0, i) = m1 * 2 + n1, #dirtyrows(mx0, i) = 1 + m0 * 2, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 0, #dirtyrows(mx0, i) ≠ 1, c0 < #c mx0, n1 < 2, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), odd(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i), #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

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 ⊦ m < 1 ↔ m = 0; (s) n < n0 ⊦ m + (* n) < (* n0) ↔ m < n0 - n; (s) ⊦ m +1 = m + 1; (s)

Proof step 52 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 53:

  #dirtyrows(mx0, i) = 1 + m0 * 2, #dirtyrows(mx0, i) = m1 * 2 + n1, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, n1 = n2 +1, #dirtyrows(mx0, i) ≠ 0, #dirtyrows(mx0, i) ≠ 1, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), n1 < 2, c0 < #c mx0, odd(#clean0rows(mx0, i)), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i), (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2 ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; ⊦ n + 0 = n; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ n0 < n → (m * n + n0 = m0 * n ↔ m = m0 ∧ n0 = 0); (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult

Proof step 53 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  #dirtyrows(mx0, i) = 1 + m0 * 2, m1 * 2 = m0 * 2, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 0, #dirtyrows(mx0, i) ≠ 1, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), c0 < #c mx0, odd(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i), #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

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) eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic ⊦ m < 1 ↔ m = 0; (s) n < n0 ⊦ m + (* n) < (* n0) ↔ m < n0 - n; (s) ⊦ m +1 = m + 1; (s)

Proof step 54 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 55:

  ⊦ m0 ≠ 0 → (m * m0 = n * m0 ↔ m = n)

• Proof step 56:

  #dirtyrows(mx0, i) = 1 + m0 * 2, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, m1 = m0, #dirtyrows(mx0, i) ≠ 0, #dirtyrows(mx0, i) ≠ 1, 2 ≠ 0, c0 < #c mx0, m1 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), odd(#clean0rows(mx0, i)), #clean1rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i), (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m1;m1 + 1) < m0, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2 ⊦

Rule argument

Additional information

Used terms: m1, 2, m0

Proof step 55 from proof countevn-maxcol0-bounded (previous step) (back to tree)

A spec-lemma

Proof step 56 from proof countevn-maxcol0-bounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  #dirtyrows(mx0, i) = 1 + m0 * 2, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) ≠ 0, #dirtyrows(mx0, i) ≠ 1, m0 + 1 < countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i), c0 < #c mx0, odd(#clean0rows(mx0, i)), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx0, i) + #dirtyrows(mx0, i), λ j. j < i) * 2 ≤ #dirtyrows(mx0, i), #clean0rows(mx0, i) + #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ #r mx0, (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ m0;m0 + 1) < m0, ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2, ∀ r. #r mx0 ≤ r + #clean1rows(mx0, i) ∧ r < #r mx0 ∧ even(r) → ¬ mx0[r, c0] < i ⊦

Rule argument

Additional information

Proof step 57 from proof countevn-maxcol0-bounded (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

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