Proof step 1 from proof max0column-countcol-big-odd (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, c < #c mx, colsorted(mx0, #c mx, mx), srowsorted(mx0, #r mx0, mx0), c ≥ c0, ¬ count(mx[c]c, λ j. j < i) ≥ #clean0rows(mx0, 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-countcol-big-odd (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, count(mx[c]c, λ j. j < i) < #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c0 < #c mx0, c < #c mx0, colsorted(mx0, #c mx0, mx), srowsorted(mx0, #r mx0, mx0), c0 ≤ 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: ⊦ 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 fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ n ≥ m ↔ m ≤ n; (s)

Proof step 3 from proof max0column-countcol-big-odd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  #r mx = #r mx0, #c mx = #c mx0, c < #c mx, c0 < #c mx, colsorted(mx0, #c mx, mx), ∀ 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) + count(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)

• Proof step 5:

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

• Proof step 7:

  #c mx = #c mx0, #r mx = #r mx0, c < #c mx0, c0 < #c mx0, #clean0rows(mx0, i) + count(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i) < #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c < #c mx, c0 < #c mx, colsorted(mx0, #c mx0, mx), colsorted(mx0, #c mx, mx), srowsorted(mx0, #r mx0, mx0), c0 ≤ c, ∀ c. c < #c mx0 → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ 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

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

Proof step 4 from proof max0column-countcol-big-odd (previous step) (back to tree)

Lemma max0column-countcol

Proof step 5 from proof max0column-countcol-big-odd (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, count(mx[c0]c, λ j. j < i) < count(mx[c1]c, λ j. j < i), c1 < #c mx0, count(mx[c]c, λ j. j < i) < #clean0rows(mx0, i) + countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c0 < #c mx0, c < #c mx0, colsorted(mx0, #c mx0, mx), srowsorted(mx0, #r mx0, mx0), c0 ≤ 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: ⊦ 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)

Proof step 6 from proof max0column-countcol-big-odd (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: c1

Proof step 7 from proof max0column-countcol-big-odd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  #c mx = #c mx0, #r mx = #r mx0, count(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c < #c mx0, c0 < #c mx0, colsorted(mx0, #c mx0, mx), srowsorted(mx0, #r mx0, mx0), c0 ≤ 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: ⊦ 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)

Proof step 8 from proof max0column-countcol-big-odd (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 9:

  srowsorted(mx, #r mx, mx), c0 < #c mx, c < #c mx, c0 < c, m ≤ n, n ≤ #r mx ⊦ count(mx[c]c, m, n, λ j. j < i) ≥ countodd(mx[c0]c, m, n, λ j. j < i)

• Proof step 10:

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

Rule argument

Additional information

Used simplifier rules: ⊦ n ≥ m ↔ m ≤ n; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ ¬ n < n; (s) Used terms: c0, #r mx, mx0, #clean0rows(mx0, i), c, i

Proof step 9 from proof max0column-countcol-big-odd (previous step) (back to tree)

Lemma rowsorted-biggercol-oddbounded

Proof step 10 from proof max0column-countcol-big-odd (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: clean0rows-bounded: ⊦ ¬ #r mx < #clean0rows(mx, i); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ m; (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 11 from proof max0column-countcol-big-odd (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: ⊦ # mx[c]c = #r mx; (s) ⊦ m ≤ m; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i

Proof step 12 from proof max0column-countcol-big-odd (previous step) (back to tree)

Lemma count-add-even-odd-ind