Proof step 1 from proof max0column-clean0rowsbounded (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  #c mx = #c mx0, #r mx = #r mx0, c0 < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx0, mx0), ¬ #clean0rows(mx, i) ≥ #clean0rows(mx0, i) + min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i)), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Proof step 2 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  #c mx = #c mx0, #r mx = #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 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 ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ n ≥ m ↔ m ≤ n; (s)

Proof step 3 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  #c mx ≠ 0, #r mx = #r mx0, #c mx = #c mx0 ⊦ scolsorted(mx, #c mx0, mx0) → ¬ #clean0rows(mx, i) < #clean0rows(mx0, i)

• Proof step 5:

  #c mx = #c mx0, #r mx = #r mx0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), scolsorted(mx, #c mx0, mx0) → ¬ #clean0rows(mx, i) < #clean0rows(mx0, i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic Used terms: mx, mx0, i

Proof step 4 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma scolsorted-clean0notls

Proof step 5 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < 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 ⊦ m < m + n ↔ n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 6 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ #r mx < #clean0rows(mx, i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: mx, i

Proof step 7 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma clean0rows-bounded

Proof step 8 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), #clean0rows(mx, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #r mx0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 9 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #clean0rows(mx, i), #clean0rows(mx, i) < #r mx → count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: mx, i

Proof step 10 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma clean0rows-notallls

Proof step 11 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), #clean0rows(mx, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx, i) < #r mx0 → count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Proof step 12 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 13:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, #clean0rows(mx, i) < #r mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #clean0rows(mx, i), #clean0rows(mx, i) < #r mx0 → count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

• Proof step 60:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ #clean0rows(mx, i) < #r mx0, #clean0rows(mx, i) < #r mx0 → count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used formulas: #clean0rows(mx, i) < #r mx0

Proof step 13 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  #c mx = #c mx0, #r mx = #r mx0, count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < 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 f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 14 from proof max0column-clean0rowsbounded (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:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∃ n. ¬(n < # mx[#clean0rows(mx, i)]r → ¬ ¬ mx[#clean0rows(mx, i)]r[n] < i) ⊦

Rule argument

Additional information

Used terms: mx[#clean0rows(mx, i)]r, λ j. ¬ j < i

Proof step 15 from proof max0column-clean0rowsbounded (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ mx[r]r[c] = mx[r, c]; (s) ⊦ # mx[r]r = #c mx; (s)

Proof step 17 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 18:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, n < #c mx0 → count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: n

Proof step 18 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Proof step 19 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 20:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < #c mx0, n < c0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

• Proof step 40:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ n < c0, ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used formulas: n < c0

Proof step 20 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n + 1 < #c mx0, n < c0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, n < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 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 f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 21 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 22:

  #r mx = #r mx0, #c mx = #c mx0, c < #c mx, c0 < #c mx, c < c0, srowsorted(mx0, #r mx0, mx0), scolsorted(mx, #c mx, mx0), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ count(mx[c]c, λ j. j < i) ≥ #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i)

• Proof step 23:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < c0, n + 1 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ n < #c mx ∧ c0 < #c mx ∧ scolsorted(mx, #c mx, mx0) ∧ (∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i))

• Proof step 25:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < c0, n + 1 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≥ #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: c0, mx0, n, mx, i

Proof step 22 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma max0column-countcol-small-even

Proof step 23 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, count(mx[n]c, λ j. j < i) < count(mx[c]c, λ j. j < i), count(mx[c0]c, λ j. j < i) < count(mx[c]c, λ j. j < i), c < #c mx0, n + 1 < #c mx0, n < c0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, n < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 24 from proof max0column-clean0rowsbounded (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 ↔ false); (s) Used terms: c

Proof step 25 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n + 1 < #c mx0, n < c0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, n < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 26 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 27:

  perm(a0, a), ordered≤(a), # a0 = # a, n < # a ⊦ a[n] < i ↔ n < count(a0, λ j. j < i)

• Proof step 28:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < c0, n + 1 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ perm(mx0[n]c, mx[n]c) ∧ ordered≤(mx[n]c) ∧ # mx0[n]c = # mx[n]c ∧ #clean0rows(mx, i) < # mx[n]c

• Proof step 33:

  #c mx = #c mx0, #r mx = #r mx0, mx[n]c[#clean0rows(mx, i)] < i ↔ #clean0rows(mx, i) < count(mx0[n]c, λ j. j < i), min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < c0, n + 1 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: mx0[n]c, mx[n]c, #clean0rows(mx, i), i

Proof step 27 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma sortedperm-count-splits

Proof step 28 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < c0, n + 1 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ perm(mx0[n]c, mx[n]c) ∧ ordered≤(mx[n]c)

Rule argument

Additional information

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

Proof step 29 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ m ≤ #c mx → ( scolsorted(mx, m, mx0) ↔ #r mx = #r mx0 ∧ #c mx = #c mx0 ∧ (∀ c. c < #c mx → (c < m ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c)))

• Proof step 31:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n + 1 < #c mx0, n < c0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, n < #c mx0, srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #c mx0 ≤ #c mx, ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → (c < #c mx0 ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c) ⊦ perm(mx0[n]c, mx[n]c) ∧ ordered≤(mx[n]c)

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) 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 lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ m < n → ¬ n < m; (s) Used terms: mx, #c mx0, mx0

Proof step 30 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma scolsorted-def

Proof step 31 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n + 1 < #c mx0, n < c0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, n < #c mx0, srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx0 → perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c) ⊦ perm(mx0[n]c, mx[n]c) ∧ ordered≤(mx[n]c)

Rule argument

Additional information

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

Proof step 32 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 33 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 34:

  ⊦ perm(x, y) → count(x, p) = count(y, p)

• Proof step 35:

  #c mx = #c mx0, #r mx = #r mx0, mx[n]c[#clean0rows(mx, i)] < i ↔ #clean0rows(mx, i) < count(mx0[n]c, λ j. j < i), min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n + 1 < #c mx0, n < c0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, n < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ¬ mx[#clean0rows(mx, i), n] < i, perm(mx0[n]c, mx[n]c) → count(mx0[n]c, λ j. j < i) = count(mx[n]c, λ j. j < i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: mx0[n]c, mx[n]c, λ j. j < i

Proof step 34 from proof max0column-clean0rowsbounded (previous step) (back to tree)

A spec-lemma

Proof step 35 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 36:

  #c mx = #c mx0, #r mx = #r mx0, mx[n]c[#clean0rows(mx, i)] < i ↔ #clean0rows(mx, i) < count(mx0[n]c, λ j. j < i), min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < c0, n + 1 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ¬ perm(mx0[n]c, mx[n]c), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mx[c]c[r] = mx[r, c]; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ¬ m < min(m, n); (s) min-a: ⊦ min(m, min(n, n0)) = min(min(m, n), n0); from specification nat-even min-c: ⊦ min(m, n) = min(n, m); from specification nat-even a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 36 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

  ⊦ m ≤ #c mx → ( scolsorted(mx, m, mx0) ↔ #r mx = #r mx0 ∧ #c mx = #c mx0 ∧ (∀ c. c < #c mx → (c < m ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c)))

• Proof step 38:

  #c mx = #c mx0, #r mx = #r mx0, mx[n]c[#clean0rows(mx, i)] < i ↔ #clean0rows(mx, i) < count(mx0[n]c, λ j. j < i), min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n + 1 < #c mx0, n < c0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, n < #c mx0, srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #c mx0 ≤ #c mx, ¬ mx[#clean0rows(mx, i), n] < i, ¬ perm(mx0[n]c, mx[n]c), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → (c < #c mx0 ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mx[c]c[r] = mx[r, c]; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n ↔ ¬ n ≤ m; (ss) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat 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 lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ m < n → ¬ n < m; (s) Used terms: mx, #c mx0, mx0

Proof step 37 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma scolsorted-def

Proof step 38 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < c0, c0 < #c mx0, n + 1 < #c mx0, count(mx0[n]c, λ j. j < i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), count(mx0[n]c, λ j. j < i) < #r mx0, srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx0[n]c, λ j. j < i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ¬ perm(mx0[n]c, mx[n]c), ∀ c. c < #c mx0 → perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m ≤ m; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ mx[c]c[r] = mx[r, c]; (s)

Proof step 39 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 40 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), c0 ≤ n, ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 41 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 42:

  #r mx = #r mx0, #c mx = #c mx0, c < #c mx, c0 < #c mx, c ≥ c0, srowsorted(mx0, #r mx0, mx0), scolsorted(mx, #c mx, mx0), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ count(mx[c]c, λ j. j < i) ≥ #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i)

• Proof step 43:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), c0 ≤ n, count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ n < #c mx ∧ c0 < #c mx ∧ n ≥ c0 ∧ scolsorted(mx, #c mx, mx0) ∧ (∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i))

• Proof step 45:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), c0 ≤ n, count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≥ #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: c0, mx0, n, mx, i

Proof step 42 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma max0column-countcol-big-odd

Proof step 43 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, count(mx[n]c, λ j. j < i) < count(mx[c]c, λ j. j < i), count(mx[c0]c, λ j. j < i) < count(mx[c]c, λ j. j < i), c < #c mx0, n < #c mx0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), c0 ≤ n, ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 44 from proof max0column-clean0rowsbounded (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 ↔ false); (s) Used terms: c

Proof step 45 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), c0 ≤ n, #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 46 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 47:

  perm(a0, a), ordered≤(a), # a0 = # a, n < # a ⊦ a[n] < i ↔ n < count(a0, λ j. j < i)

• Proof step 48:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), c0 ≤ n, count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ perm(mx0[n]c, mx[n]c) ∧ ordered≤(mx[n]c) ∧ # mx0[n]c = # mx[n]c ∧ #clean0rows(mx, i) < # mx[n]c

• Proof step 53:

  #c mx = #c mx0, #r mx = #r mx0, mx[n]c[#clean0rows(mx, i)] < i ↔ #clean0rows(mx, i) < count(mx0[n]c, λ j. j < i), min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), c0 ≤ n, count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: mx0[n]c, mx[n]c, #clean0rows(mx, i), i

Proof step 47 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma sortedperm-count-splits

Proof step 48 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), c0 ≤ n, count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ perm(mx0[n]c, mx[n]c) ∧ ordered≤(mx[n]c)

Rule argument

Additional information

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

Proof step 49 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 50:

  ⊦ m ≤ #c mx → ( scolsorted(mx, m, mx0) ↔ #r mx = #r mx0 ∧ #c mx = #c mx0 ∧ (∀ c. c < #c mx → (c < m ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c)))

• Proof step 51:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), c0 ≤ n, #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #c mx0 ≤ #c mx, ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → (c < #c mx0 ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c) ⊦ perm(mx0[n]c, mx[n]c) ∧ ordered≤(mx[n]c)

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) 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 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; (s) Used terms: mx, #c mx0, mx0

Proof step 50 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma scolsorted-def

Proof step 51 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), c0 ≤ n, #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx0 → perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c) ⊦ perm(mx0[n]c, mx[n]c) ∧ ordered≤(mx[n]c)

Rule argument

Additional information

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

Proof step 52 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 53 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 54:

  ⊦ perm(x, y) → count(x, p) = count(y, p)

• Proof step 55:

  #c mx = #c mx0, #r mx = #r mx0, mx[n]c[#clean0rows(mx, i)] < i ↔ #clean0rows(mx, i) < count(mx0[n]c, λ j. j < i), min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), c0 ≤ n, #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ¬ mx[#clean0rows(mx, i), n] < i, perm(mx0[n]c, mx[n]c) → count(mx0[n]c, λ j. j < i) = count(mx[n]c, λ j. j < i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: mx0[n]c, mx[n]c, λ j. j < i

Proof step 54 from proof max0column-clean0rowsbounded (previous step) (back to tree)

A spec-lemma

Proof step 55 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 56:

  #c mx = #c mx0, #r mx = #r mx0, mx[n]c[#clean0rows(mx, i)] < i ↔ #clean0rows(mx, i) < count(mx0[n]c, λ j. j < i), min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), c0 ≤ n, count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ¬ perm(mx0[n]c, mx[n]c), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mx[c]c[r] = mx[r, c]; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ¬ m < min(m, n); (s) min-a: ⊦ min(m, min(n, n0)) = min(min(m, n), n0); from specification nat-even min-c: ⊦ min(m, n) = min(n, m); from specification nat-even a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 56 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 57:

  ⊦ m ≤ #c mx → ( scolsorted(mx, m, mx0) ↔ #r mx = #r mx0 ∧ #c mx = #c mx0 ∧ (∀ c. c < #c mx → (c < m ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c)))

• Proof step 58:

  #c mx = #c mx0, #r mx = #r mx0, mx[n]c[#clean0rows(mx, i)] < i ↔ #clean0rows(mx, i) < count(mx0[n]c, λ j. j < i), min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, n < #c mx0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), c0 ≤ n, #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #c mx0 ≤ #c mx, ¬ mx[#clean0rows(mx, i), n] < i, ¬ perm(mx0[n]c, mx[n]c), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → (c < #c mx0 ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mx[c]c[r] = mx[r, c]; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n ↔ ¬ n ≤ m; (ss) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat 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 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; (s) Used terms: mx, #c mx0, mx0

Proof step 57 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma scolsorted-def

Proof step 58 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  #c mx = #c mx0, #r mx = #r mx0, min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx0, i) < #r mx0, #clean0rows(mx, i) < #r mx0, n < #c mx0, count(mx0[n]c, λ j. j < i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), count(mx0[n]c, λ j. j < i) < #r mx0, srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ count(mx[n]c, λ j. j < i), c0 ≤ n, count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx0[n]c, λ j. j < i) ≤ #clean0rows(mx, i), ¬ mx[#clean0rows(mx, i), n] < i, ¬ perm(mx0[n]c, mx[n]c), ∀ c. c < #c mx0 → perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m ≤ m; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ mx[c]c[r] = mx[r, c]; (s)

Proof step 59 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 60 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  #c mx = #c mx0, #clean0rows(mx, i) = #r mx0, #r mx = #clean0rows(mx, i), min (countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i)) ≠ 0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #clean0rows(mx, i), mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < n; (s) ⊦ m ≤ m; (s) 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) ⊦ m < n → n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 61 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 62:

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

• Proof step 63:

  #c mx = #c mx0, #clean0rows(mx, i) = #r mx0, #r mx = #clean0rows(mx, i), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i), min (countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i)) ≠ 0, c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #clean0rows(mx, i), mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 62 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma count-add-even-odd-ind

Proof step 63 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 64:

  n ≤ m, m ≤ # x ⊦ ¬ m - n < count(x, n, m, p)

• Proof step 65:

  #c mx = #c mx0, #clean0rows(mx, i) = #r mx0, #r mx = #clean0rows(mx, i), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i), min (countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i)) ≠ 0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #clean0rows(mx, i), mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ #clean0rows(mx, i) - #clean0rows(mx0, i) < count(mx[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: clean0rows-bounded: ⊦ ¬ #r mx < #clean0rows(mx, i); ⊦ # mx[c]c = #r mx; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) Used terms: #clean0rows(mx0, i), #clean0rows(mx, i), mx[c0]c, λ j. j < i

Proof step 64 from proof max0column-clean0rowsbounded (previous step) (back to tree)

A spec-lemma

Proof step 65 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

  #c mx = #c mx0, #clean0rows(mx, i) = #r mx0, #r mx = #clean0rows(mx, i), countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i), count(mx[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i)), c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #clean0rows(mx, i), mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[c0]c, #clean0rows(mx0, i), #clean0rows(mx, i), λ j. j < i) + #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < 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 ⊦ m + n < m + n0 ↔ n < n0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 66 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 67:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i), #r mx < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i)), c0 < #c mx0, count(mx[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i) < min(countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx, mx0), count(mx[c0]c, #clean0rows(mx0, i), #r mx, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx, #clean0rows(mx0, i) ≤ #r mx, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Proof step 67 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c0 < #c mx0, #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #r mx0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < 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 ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n → n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic

Proof step 68 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 69:

  ⊦ perm(x, y) → count(x, p) = count(y, p)

• Proof step 70:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #r mx0, count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, perm(mx0[c0]c, mx[c0]c) → count(mx0[c0]c, λ j. j < i) = count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: mx0[c0]c, mx[c0]c, λ j. j < i

Proof step 69 from proof max0column-clean0rowsbounded (previous step) (back to tree)

A spec-lemma

Proof step 70 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 71:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c0 < #c mx0, #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #r mx0, ¬ perm(mx0[c0]c, mx[c0]c), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

• Proof step 75:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), count(mx0[c0]c, λ j. j < i) = count(mx[c0]c, λ j. j < i), c0 < #c mx0, #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #r mx0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Proof step 71 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

  ⊦ m ≤ #c mx → ( scolsorted(mx, m, mx0) ↔ #r mx = #r mx0 ∧ #c mx = #c mx0 ∧ (∀ c. c < #c mx → (c < m ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c)))

• Proof step 73:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #r mx0, count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, #c mx0 ≤ #c mx, ¬ perm(mx0[c0]c, mx[c0]c), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → (c < #c mx0 ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) 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 lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ m < n → ¬ n < m; (s) Used terms: mx, #c mx0, mx0

Proof step 72 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma scolsorted-def

Proof step 73 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #r mx0, count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, ¬ perm(mx0[c0]c, mx[c0]c), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx0 → perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c) ⊦

Rule argument

Additional information

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

Proof step 74 from proof max0column-clean0rowsbounded (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 75 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 76:

  ⊦ count(x, p) = count(x, 0, # x, p)

• Proof step 77:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), count(mx0[c0]c, 0, # mx0[c0]c, λ j. j < i) = count(mx[c0]c, λ j. j < i), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #r mx0, count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 76 from proof max0column-clean0rowsbounded (previous step) (back to tree)

A spec-lemma

Proof step 77 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 78:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), count(mx0[c0]c, 0, #r mx0, λ j. j < i) = count(mx[c0]c, λ j. j < i), c0 < #c mx0, #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #r mx0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx0[c0]c, 0, #r mx0, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 78 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 79:

  ⊦ count(x, p) = count(x, 0, # x, p)

• Proof step 80:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), count(mx0[c0]c, 0, #r mx0, λ j. j < i) = count(mx[c0]c, 0, # mx[c0]c, λ j. j < i), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #r mx0, count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx0[c0]c, 0, #r mx0, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: mx[c0]c, λ j. j < i

Proof step 79 from proof max0column-clean0rowsbounded (previous step) (back to tree)

A spec-lemma

Proof step 80 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 81:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), count(mx0[c0]c, 0, #r mx0, λ j. j < i) = count(mx[c0]c, 0, #r mx0, λ j. j < i), c0 < #c mx0, #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #r mx0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, 0, #r mx0, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 81 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 82:

  m ≤ n, n ≤ n0, n0 ≤ # x ⊦ count(x, m, n, p) + count(x, n, n0, p) = count(x, m, n0, p)

• Proof step 83:

  #c mx = #c mx0, #r mx = #r mx0, count(mx0[c0]c, 0, #clean0rows(mx0, i), λ j. j < i) + count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx[c0]c, 0, #r mx0, λ j. j < i), countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, 0 ≤ #clean0rows(mx0, i), #clean0rows(mx0, i) ≤ #r mx0, #r mx0 ≤ # mx0[c0]c, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, 0, #r mx0, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ m; (s) ⊦ # mx[c]c = #r mx; (s) ⊦ m ≤ m; (s) Used terms: #r mx0, λ j. j < i, #clean0rows(mx0, i), 0, mx0[c0]c

Proof step 82 from proof max0column-clean0rowsbounded (previous step) (back to tree)

A spec-lemma

Proof step 83 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 84:

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

• Proof step 85:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #clean0rows(mx0, i) + count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx[c0]c, 0, #r mx0, λ j. j < i), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #r mx0 ≤ # mx0[c0]c, #clean0rows(mx0, i) ≤ #r mx0, 0 ≤ #clean0rows(mx0, i), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #clean0rows(mx0, i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, 0, #r mx0, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ m; (s) ⊦ # mx[c]c = #r mx; (s) ⊦ m ≤ m; (s) Used terms: i, mx0, c0, #clean0rows(mx0, i)

Proof step 84 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma count0-leq-clean0-ind

Proof step 85 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 86:

  m ≤ n, n ≤ n0, n0 ≤ # x ⊦ count(x, m, n, p) + count(x, n, n0, p) = count(x, m, n0, p)

• Proof step 87:

  #c mx = #c mx0, #r mx = #r mx0, #clean0rows(mx0, i) + count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx[c0]c, 0, #clean0rows(mx0, i), λ j. j < i) + count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c0 < #c mx0, count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx0, i), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, #r mx0 ≤ # mx0[c0]c, 0 ≤ #clean0rows(mx0, i), #clean0rows(mx0, i) ≤ #r mx0, #r mx0 ≤ # mx[c0]c, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, 0, #clean0rows(mx0, i), λ j. j < i) + count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 86 from proof max0column-clean0rowsbounded (previous step) (back to tree)

A spec-lemma

Proof step 87 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 88:

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

• Proof step 89:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #clean0rows(mx0, i) + count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx[c0]c, 0, #clean0rows(mx0, i), λ j. j < i) + count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #r mx0 ≤ # mx[c0]c, #clean0rows(mx0, i) ≤ #r mx0, 0 ≤ #clean0rows(mx0, i), #r mx0 ≤ # mx0[c0]c, count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #clean0rows(mx0, i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, 0, #clean0rows(mx0, i), λ j. j < i) + count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ⊦ c0 < #c mx ∧ #clean0rows(mx0, i) ≤ #clean0rows(mx, i)

• Proof step 93:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #clean0rows(mx0, i) + count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = #clean0rows(mx0, i) + count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, c0 < #c mx, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #r mx0 ≤ # mx[c0]c, #clean0rows(mx0, i) ≤ #r mx0, 0 ≤ #clean0rows(mx0, i), #r mx0 ≤ # mx0[c0]c, count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #clean0rows(mx0, i), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ #clean0rows(mx0, i) + count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: i, mx, c0, #clean0rows(mx0, i)

Proof step 88 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma count0-leq-clean0-ind

Proof step 89 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 90:

  #c mx = #c mx0, #r mx = #r mx0, #clean0rows(mx0, i) + count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx[c0]c, 0, #clean0rows(mx0, i), λ j. j < i) + count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c0 < #c mx0, count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx0, i), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, #r mx0 ≤ # mx0[c0]c, 0 ≤ #clean0rows(mx0, i), #clean0rows(mx0, i) ≤ #r mx0, #r mx0 ≤ # mx[c0]c, ¬ #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, 0, #clean0rows(mx0, i), λ j. j < i) + count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 ≤ m; (s) ⊦ # mx[c]c = #r mx; (s) ⊦ m ≤ m; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ ¬ n < n; (s)

Proof step 90 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 91:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #clean0rows(mx0, i) + count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx[c0]c, 0, #clean0rows(mx0, i), λ j. j < i) + count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #clean0rows(mx, i) < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx, i) < #r mx0, #clean0rows(mx, i) + 1 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #r mx0, count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, 0, #clean0rows(mx0, i), λ j. j < i) + count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ m; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ # mx[c]c = #r mx; (s) ⊦ 0 ≤ m; (s)

Proof step 91 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 92:

  #c mx ≠ 0, #r mx = #r mx0, #c mx = #c mx0 ⊦ scolsorted(mx, #c mx0, mx0) → ¬ #clean0rows(mx, i) < #clean0rows(mx0, i)

Rule argument

Additional information

Used simplifier rules: f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic Used terms: mx, i, mx0

Proof step 92 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Lemma scolsorted-clean0notls

Proof step 93 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 94:

  #c mx = #c mx0, #r mx = #r mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), c0 < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #r mx0, count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ #clean0rows(mx0, i) + count(mx[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ # mx[c]c = #r mx; (s) ⊦ 0 ≤ m; (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 94 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 95:

  #c mx = #c mx0, #r mx = #r mx0, count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c0 < #c mx0, countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) + #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #r mx0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ #clean0rows(mx0, i) + countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ⊦

Rule argument

Additional information

Proof step 95 from proof max0column-clean0rowsbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 96:

  #c mx = #c mx0, #r mx = #r mx0, count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) = countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c0 < #c mx0, #r mx0 < #clean0rows(mx0, i) + min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < min (countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) ≤ #r mx0, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ #clean0rows(mx0, i) + count(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < 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 ⊦ m + n < m + n0 ↔ n < n0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat

Proof step 96 from proof max0column-clean0rowsbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 97:

  ⊦ m < n → min(m, n) = m

Rule argument

Additional information

Used simplifier rules: lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ m +1 = m + 1; (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 ⊦ ¬ m < n → min(m, n) = n; (s) min-a: ⊦ min(m, min(n, n0)) = min(min(m, n), n0); from specification nat-even min-c: ⊦ min(m, n) = min(n, m); from specification nat-even ⊦ m < n ↔ ¬ n ≤ m; (ss) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat Used terms: countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)

Proof step 97 from proof max0column-clean0rowsbounded (previous step) (back to tree)

A spec-lemma