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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, c0 < #c mx, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

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

• Proof step 4:

  #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, c0 < #c mx, ¬ #r mx < #clean1rows(mx, i), ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: mx, i

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

Lemma clean1rows-bounded

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, c0 < #c mx, #clean1rows(mx, i) ≤ #r mx, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → 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 ⊦ m < n ↔ ¬ n ≤ m; (ss)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

  #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, c0 < #c mx, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, #clean1rows(mx, i) ≤ #r mx, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

• Proof step 22:

  #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, c0 < #c mx, #clean1rows(mx, i) ≤ #r mx, ¬ #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

Rule argument

Additional information

Used formulas: #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, c0 < #c mx, #clean1rows(mx, i) ≤ #r mx, #clean1rows(mx, i) + (#r mx - #clean1rows(mx, i) + 1) + 1 = #r mx → count(mx[#r mx - #clean1rows(mx, i) + 1]r, λ j. j < i) ≠ 0, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: mx, i, #r mx - #clean1rows(mx, i) + 1

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

Lemma clean1rows-notallge

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, count(mx[#r mx - #clean1rows(mx, i) + 1]r, λ j. j < i) ≠ 0, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, c0 < #c mx, #clean1rows(mx, i) ≤ #r mx, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → 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 n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1; (s) ⊦ ¬ m + n < m; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m + 1 ≤ n ↔ m < n; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

  #r mx = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, count(mx[n0]r, λ j. j < i) ≠ 0, c0 < #c mx, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, #clean1rows(mx, i) ≤ #r mx, #clean1rows(mx, i) + 1 ≤ #r mx, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ m = m + n ↔ n = 0; (s) ⊦ m + m0 < n → ¬ n + n0 < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: #r mx, #clean1rows(mx, i) + 1, n0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  #r mx = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, count(mx[n0]r, λ j. j < i) ≠ 0, #clean1rows(mx, i) < #r mx, c0 < #c mx, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, count(mx[c0]c, λ j. j < i) ≤ n0, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ ¬ m + n < m; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m < n → m ≤ n; (s) ⊦ m + 1 ≤ n ↔ m < n; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  #r mx = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, c0 < #c mx, #clean1rows(mx, i) < #r mx, count(mx[c0]c, λ j. j < i) ≤ n0, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∃ n. ¬(n < # mx[n0]r → ¬ mx[n0]r[n] < i) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  #r mx = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, #clean1rows(mx, i) < #r mx, c0 < #c mx, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, mx[n0, n] < i, n < #c mx, count(mx[c0]c, λ j. j < i) ≤ n0, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

Rule argument

Additional information

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

Proof step 14 from proof max0column-determines-clean1rows (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 15:

  #r mx = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, n < #c mx, mx[n0, n] < i, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, c0 < #c mx, #clean1rows(mx, i) < #r mx, count(mx[c0]c, λ j. j < i) ≤ n0, n < #c mx → count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: n

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  #r mx = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, #clean1rows(mx, i) < #r mx, c0 < #c mx, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, mx[n0, n] < i, n < #c mx, count(mx[c0]c, λ j. j < i) ≤ n0, count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), count(mx[n]c, λ j. j < i) ≤ n0, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

Rule argument

Additional information

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

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

  #r mx = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, n < #c mx, mx[n0, n] < i, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, c0 < #c mx, #clean1rows(mx, i) < #r mx, count(mx[n]c, λ j. j < i) ≤ n0, count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), count(mx[c0]c, λ j. j < i) ≤ n0, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ perm(mx[n]c, mx[n]c) ∧ ordered≤(mx[n]c) ∧ # mx[n]c = # mx[n]c ∧ n0 < # mx[n]c

Rule argument

Additional information

Used simplifier rules: ⊦ mx[c]c[r] = mx[r, c]; (s) ⊦ m ≤ n → (n < m ↔ false); (s) Used terms: mx[n]c, mx[n]c, n0, i

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

Lemma sortedperm-count-splits

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  #r mx = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, #clean1rows(mx, i) < #r mx, c0 < #c mx, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, mx[n0, n] < i, n < #c mx, count(mx[c0]c, λ j. j < i) ≤ n0, count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), count(mx[n]c, λ j. j < i) ≤ n0, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦ ordered≤(mx[n]c) ∧ n0 < #r mx

Rule argument

Additional information

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

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

User applied rule all left

And obtained the following new goals

• Proof step 20:

  #r mx = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, n < #c mx, mx[n0, n] < i, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, c0 < #c mx, #clean1rows(mx, i) < #r mx, count(mx[n]c, λ j. j < i) ≤ n0, count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), count(mx[c0]c, λ j. j < i) ≤ n0, n < #c mx → ordered≤(mx[n]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ ordered≤(mx[n]c) ∧ n0 < #r mx

Rule argument

Additional information

Used terms: n

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  #r mx = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, #clean1rows(mx, i) < #r mx, c0 < #c mx, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < #r mx, mx[n0, n] < i, n < #c mx, #clean1rows(mx, i) < n0, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) < n0, ordered≤(mx[n]c), count(mx[c0]c, λ j. j < i) ≤ n0, count(mx[n]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), count(mx[n]c, λ j. j < i) ≤ n0, #r mx ≤ n0, ∀ c. c < #c mx → 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 fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

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

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, count(mx[c0]c, λ j. j < i) ≠ 0, #r mx < #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i), c0 < #c mx, #clean1rows(mx, i) ≤ #r mx, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

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) ⊦ 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 ⊦ m ≠ n → (m < n ↔ ¬ n < m); (ss)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 24:

  #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, count(mx[c0]c, λ j. j < i) ≠ 0, c0 < #c mx, #r mx < #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i), #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) > #r mx, #clean1rows(mx, i) ≤ #r mx, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m > n ↔ n < m; (s) ⊦ m ≠ n → (m < n ↔ ¬ n < m); (ss) ⊦ m < n → ¬ n < m; (s) Used formulas: #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) > #r mx

Proof step 24 from proof max0column-determines-clean1rows (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, count(mx[c0]c, λ j. j < i) ≠ 0, c0 < #c mx, #r mx < #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i), #clean1rows(mx, i) ≤ #r mx, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m > n ↔ n < m; (s)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

  #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, count(mx[c0]c, λ j. j < i) ≠ 0, #r mx < #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i), c0 < #c mx, #clean1rows(mx, i) ≤ #r mx, #r mx ≤ #clean1rows(mx, i) + (count(mx[c0]c, λ j. j < i) - 1) ∧ count(mx[c0]c, λ j. j < i) - 1 < #r mx → count(mx[count(mx[c0]c, λ j. j < i) - 1]r, λ j. j < i) = 0, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: mx, i, count(mx[c0]c, λ j. j < i) - 1

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

Lemma clean1rows-allge

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, count(mx[c0]c, λ j. j < i) ≠ 0, c0 < #c mx, #r mx < #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i), #clean1rows(mx, i) ≤ #r mx, #r mx ≤ #clean1rows(mx, i) + (count(mx[c0]c, λ j. j < i) - 1) ∧ ¬ #r mx < count(mx[c0]c, λ j. j < i) → count(mx[count(mx[c0]c, λ j. j < i) - 1]r, λ j. j < i) = 0, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i), ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

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

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 29:

  count(mx[c0]c, λ j. j < i) = m + 1, #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) ≠ #r mx, count(mx[c0]c, λ j. j < i) ≠ 0, #r mx < #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i), c0 < #c mx, #clean1rows(mx, i) ≤ #r mx, #r mx ≤ #clean1rows(mx, i) + m ∧ ¬ #r mx < count(mx[c0]c, λ j. j < i) → count(mx[m]r, λ j. j < i) = 0, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: count(mx[c0]c, λ j. j < i), m

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  count(mx[c0]c, λ j. j < i) = m + 1, #clean1rows(mx, i) + m + 1 ≠ #r mx, c0 < #c mx, #r mx ≤ #clean1rows(mx, i) + m, #clean1rows(mx, i) ≤ #r mx, m < #r mx → count(mx[m]r, λ j. j < i) = 0, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ m + 1, ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

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; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ ¬ m + n < m; (s) ⊦ m + 1 ≠ 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 30 from proof max0column-determines-clean1rows (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 31:

  ⊦ ¬ # x < count(x, p)

• Proof step 32:

  count(mx[c0]c, λ j. j < i) = m + 1, #clean1rows(mx, i) + m + 1 ≠ #r mx, c0 < #c mx, #clean1rows(mx, i) ≤ #r mx, #r mx ≤ #clean1rows(mx, i) + m, ¬ # mx[c0]c < count(mx[c0]c, λ j. j < i), m < #r mx → count(mx[m]r, λ j. j < i) = 0, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ m + 1 ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  count(mx[c0]c, λ j. j < i) = m + 1, count(mx[m]r, λ j. j < i) = 0, #clean1rows(mx, i) ≠ 0, #clean1rows(mx, i) + m + 1 ≠ #r mx, #clean1rows(mx, i) + m ≠ 0, c0 < #c mx, m < #r mx, 1 ≤ #clean1rows(mx, i) + m, #clean1rows(mx, i) ≤ #r mx, #r mx ≤ #clean1rows(mx, i) + m, 1 ≤ #clean1rows(mx, i), 1 ≤ #r mx, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ m + 1 ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

• Proof step 35:

  count(mx[c0]c, λ j. j < i) = m + 1, #clean1rows(mx, i) ≠ 0, #clean1rows(mx, i) + m + 1 ≠ #r mx, #clean1rows(mx, i) + m ≠ 0, m < #r mx, c0 < #c mx, 1 ≤ #r mx, 1 ≤ #clean1rows(mx, i), #r mx ≤ #clean1rows(mx, i) + m, #clean1rows(mx, i) ≤ #r mx, 1 ≤ #clean1rows(mx, i) + m, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ m + 1, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ n. n < # mx[m]r → ¬ mx[m]r[n] < i ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  count(mx[c0]c, λ j. j < i) = m + 1, #clean1rows(mx, i) ≠ 0, #clean1rows(mx, i) + m + 1 ≠ #r mx, #clean1rows(mx, i) + m ≠ 0, c0 < #c mx, m < #r mx, 1 ≤ #clean1rows(mx, i) + m, #clean1rows(mx, i) ≤ #r mx, #r mx ≤ #clean1rows(mx, i) + m, 1 ≤ #clean1rows(mx, i), 1 ≤ #r mx, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ m + 1, ∀ n. n < #c mx → ¬ mx[m, n] < i ⊦

Rule argument

Additional information

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

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 37:

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

• Proof step 38:

  count(mx[c0]c, λ j. j < i) = m + 1, #clean1rows(mx, i) ≠ 0, #clean1rows(mx, i) + m + 1 ≠ #r mx, #clean1rows(mx, i) + m ≠ 0, m < #r mx, c0 < #c mx, 1 ≤ #r mx, 1 ≤ #clean1rows(mx, i), #r mx ≤ #clean1rows(mx, i) + m, #clean1rows(mx, i) ≤ #r mx, 1 ≤ #clean1rows(mx, i) + m, ∀ n. n < #c mx → ¬ mx[m, n] < i, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ m + 1, ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦ perm(mx[c0]c, mx[c0]c) ∧ ordered≤(mx[c0]c) ∧ # mx[c0]c = # mx[c0]c ∧ count(mx[c0]c, λ j. j < i) - 1 < # mx[c0]c

• Proof step 40:

  mx[c0]c[count(mx[c0]c, λ j. j < i) - 1] < i ↔ count(mx[c0]c, λ j. j < i) - 1 < count(mx[c0]c, λ j. j < i), count(mx[c0]c, λ j. j < i) = m + 1, #clean1rows(mx, i) ≠ 0, #clean1rows(mx, i) + m + 1 ≠ #r mx, #clean1rows(mx, i) + m ≠ 0, m < #r mx, c0 < #c mx, 1 ≤ #r mx, 1 ≤ #clean1rows(mx, i), #r mx ≤ #clean1rows(mx, i) + m, #clean1rows(mx, i) ≤ #r mx, 1 ≤ #clean1rows(mx, i) + m, ∀ n. n < #c mx → ¬ mx[m, n] < i, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ m + 1, ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

Rule argument

Additional information

Used terms: mx[c0]c, mx[c0]c, count(mx[c0]c, λ j. j < i) - 1, i

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

Lemma sortedperm-count-splits

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  count(mx[c0]c, λ j. j < i) = m + 1, #clean1rows(mx, i) ≠ 0, #clean1rows(mx, i) + m ≠ 0, #clean1rows(mx, i) + m + 1 ≠ #r mx, m < #r mx, c0 < #c mx, 1 ≤ #r mx, 1 ≤ #clean1rows(mx, i), #r mx ≤ #clean1rows(mx, i) + m, #clean1rows(mx, i) ≤ #r mx, 1 ≤ #clean1rows(mx, i) + m, ¬ ordered≤(mx[c0]c), ∀ n. n < #c mx → ¬ mx[m, n] < i, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ m + 1, ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

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 + 1 ↔ ¬ n < m; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ ¬ m < n → ¬ m + m0 < n; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ # mx[c]c = #r mx; (s) ⊦ perm(x, x); (s)

Proof step 39 from proof max0column-determines-clean1rows (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 40 from proof max0column-determines-clean1rows (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  count(mx[c0]c, λ j. j < i) = m + 1, #clean1rows(mx, i) ≠ 0, #clean1rows(mx, i) + m ≠ 0, #clean1rows(mx, i) + m + 1 ≠ #r mx, m < #r mx, c0 < #c mx, mx[m, c0] < i, 1 ≤ #r mx, 1 ≤ #clean1rows(mx, i), #r mx ≤ #clean1rows(mx, i) + m, #clean1rows(mx, i) ≤ #r mx, 1 ≤ #clean1rows(mx, i) + m, ∀ n. n < #c mx → ¬ mx[m, n] < i, ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ m + 1, ∀ c. c < #c mx → ordered≤(mx[c]c) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ mx[c]c[r] = mx[r, c]; (s) ⊦ ¬ n < n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ ¬ m < n → ¬ m + m0 < n; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: c0