Proof step 1 from proof rowsorted-biggercol-oddbounded (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (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; (ss) ⊦ n ≥ m ↔ m ≤ n; (s)

Proof step 3 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  c0 + 1 < #c mx, c0 < #c mx, c < #c mx, c0 < c, count(mx[c]c, m, n0 +1, λ j. j < i) < countodd(mx[c0]c, m, n0 +1, λ j. j < i), srowsorted(mx, #r mx, mx), m ≤ n0 +1, n0 +1 ≤ #r mx, m ≤ #r mx, ∀ mx, c, m, i, c0. ¬ ( count(mx[c]c, m, n0, λ j. j < i) < countodd(mx[c0]c, m, n0, λ j. j < i) ∧ c0 < c ∧ c < #c mx ∧ c0 < #c mx ∧ c0 + 1 < #c mx ∧ srowsorted(mx, #r mx, mx) ∧ m ≤ #r mx ∧ n0 ≤ #r mx ∧ m ≤ n0) ⊦

Rule argument

Additional information

Used simplifier rules: countodd-base: m ≤ # a ⊦ countodd(a, m, m, p) = 0; nat freely generated by 0, +1;; ⊦ m ≤ 0 ↔ m = 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ # mx[c]c = #r mx; (s) ⊦ 0 ≤ m; (s)

Proof step 4 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  count(mx[c]c, m, n0 + 1, λ j. j < i) < countodd(mx[c0]c, m, n0 + 1, λ j. j < i), n0 < #r mx, c0 + 1 < #c mx, c0 < #c mx, c < #c mx, c0 < c, srowsorted(mx, #r mx, mx), m ≤ n0 + 1, m ≤ #r mx, ∀ mx0, c1, m0, i0, c2. ¬ count(mx0[c1]c, m0, n0, λ j. j < i0) < countodd(mx0[c2]c, m0, n0, λ j. j < i0) ∨ ¬ c2 < c1 ∨ ¬ c1 < #c mx0 ∨ ¬ c2 < #c mx0 ∨ ¬ c2 + 1 < #c mx0 ∨ ¬ srowsorted(mx0, #r mx0, mx0) ∨ ¬ m0 ≤ #r mx0 ∨ ¬ n0 ≤ #r mx0 ∨ ¬ m0 ≤ n0 ⊦

Rule argument

Additional information

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

Proof step 5 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  m ≤ n, n ≤ # x ⊦ count(x, m, n + 1, p) = count(x, m, n, p) + (p(x[n]) ⊃ 1;0)

• Proof step 7:

  c0 < c, c < #c mx, c0 < #c mx, c0 + 1 < #c mx, n0 < #r mx, count(mx[c]c, m, n0, λ j. j < i) + (mx[c]c[n0] < i ⊃ 1;0) < countodd(mx[c0]c, m, n0 + 1, λ j. j < i), srowsorted(mx, #r mx, mx), m ≤ #r mx, m ≤ n0 + 1, m ≤ n0, n0 ≤ # mx[c]c, ∀ mx0, c1, m0, i0, c2. ¬ count(mx0[c1]c, m0, n0, λ j. j < i0) < countodd(mx0[c2]c, m0, n0, λ j. j < i0) ∨ ¬ c2 < c1 ∨ ¬ c1 < #c mx0 ∨ ¬ c2 < #c mx0 ∨ ¬ c2 + 1 < #c mx0 ∨ ¬ srowsorted(mx0, #r mx0, mx0) ∨ ¬ m0 ≤ #r mx0 ∨ ¬ n0 ≤ #r mx0 ∨ ¬ m0 ≤ n0 ⊦

Rule argument

Additional information

Used simplifier rules: countodd-base: m ≤ # a ⊦ countodd(a, m, m, p) = 0; ⊦ m < n → m ≤ n; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat 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 + 1 ≠ 0; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ n < n; (s) m ≤ # x ⊦ count(x, m, m, p) = 0; (s) ⊦ # mx[c]c = #r mx; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: mx[c]c, m, n0, λ j. j < i

Proof step 6 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  m < #r mx, count(mx[c]c, m, n0, λ j. j < i) + (mx[n0, c] < i ⊃ 1;0) < countodd(mx[c0]c, m, n0, λ j. j < i) + (odd(n0) ∧ mx[n0, c0] < i ⊃ 1;0), c0 < c, c < #c mx, c0 < #c mx, c0 + 1 < #c mx, n0 < #r mx, srowsorted(mx, #r mx, mx), m ≤ n0 + 1, m ≤ n0, ∀ mx0, c1, m0, i0, c2. ¬ count(mx0[c1]c, m0, n0, λ j. j < i0) < countodd(mx0[c2]c, m0, n0, λ j. j < i0) ∨ ¬ c2 < c1 ∨ ¬ c1 < #c mx0 ∨ ¬ c2 < #c mx0 ∨ ¬ c2 + 1 < #c mx0 ∨ ¬ srowsorted(mx0, #r mx0, mx0) ∨ ¬ m0 ≤ #r mx0 ∨ ¬ n0 ≤ #r mx0 ∨ ¬ m0 ≤ n0 ⊦

Rule argument

Additional information

Used simplifier rules: countodd-rec: m ≤ n, n ≤ # a ⊦ countodd(a, m, n + 1, p) = countodd(a, m, n, p) + (odd(n) ∧ p(a[n]) ⊃ 1;0); ⊦ m < n → m ≤ n; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ mx[c]c[r] = mx[r, c]; (s) ⊦ # mx[c]c = #r mx; (s)

Proof step 8 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 9:

  n0 < #r mx, c0 + 1 < #c mx, c0 < #c mx, c < #c mx, c0 < c, count(mx[c]c, m, n0, λ j. j < i) + (mx[n0, c] < i ⊃ 1;0) < countodd(mx[c0]c, m, n0, λ j. j < i) + (odd(n0) ∧ mx[n0, c0] < i ⊃ 1;0), m < #r mx, srowsorted(mx, #r mx, mx), m ≤ n0, m ≤ n0 + 1, ¬ count(mx[c]c, m, n0, λ j. j < i) < countodd(mx[c0]c, m, n0, λ j. j < i) ∨ ¬ c0 < c ∨ ¬ c < #c mx ∨ ¬ c0 < #c mx ∨ ¬ c0 + 1 < #c mx ∨ ¬ srowsorted(mx, #r mx, mx) ∨ ¬ m ≤ #r mx ∨ ¬ n0 ≤ #r mx ∨ ¬ m ≤ n0 ⊦

Rule argument

Additional information

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

Proof step 9 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  m < #r mx, count(mx[c]c, m, n0, λ j. j < i) + (mx[n0, c] < i ⊃ 1;0) < countodd(mx[c0]c, m, n0, λ j. j < i) + (odd(n0) ∧ mx[n0, c0] < i ⊃ 1;0), c0 < c, c < #c mx, c0 < #c mx, c0 + 1 < #c mx, n0 < #r mx, srowsorted(mx, #r mx, mx), m ≤ n0 + 1, m ≤ n0, countodd(mx[c0]c, m, n0, λ j. j < i) ≤ count(mx[c]c, m, n0, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → m ≤ n; (s)

Proof step 10 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  n0 < #r mx, c0 + 1 < #c mx, c0 < #c mx, c < #c mx, c0 < c, m < #r mx, count(mx[c]c, m, n0, λ j. j < i) + 1 < countodd(mx[c0]c, m, n0, λ j. j < i) + (odd(n0) ∧ mx[n0, c0] < i ⊃ 1;0), mx[n0, c] < i, srowsorted(mx, #r mx, mx), countodd(mx[c0]c, m, n0, λ j. j < i) ≤ count(mx[c]c, m, n0, λ j. j < i), m ≤ n0, m ≤ n0 + 1 ⊦

• Proof step 12:

  n0 < #r mx, c0 + 1 < #c mx, c0 < #c mx, c < #c mx, c0 < c, m < #r mx, count(mx[c]c, m, n0, λ j. j < i) + 0 < countodd(mx[c0]c, m, n0, λ j. j < i) + (odd(n0) ∧ mx[n0, c0] < i ⊃ 1;0), srowsorted(mx, #r mx, mx), countodd(mx[c0]c, m, n0, λ j. j < i) ≤ count(mx[c]c, m, n0, λ j. j < i), m ≤ n0, m ≤ n0 + 1, ¬ mx[n0, c] < i ⊦

Rule argument

Additional information

Proof step 11 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ n + 0 = n; (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 ≠ 0; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m ≤ m0 ∧ n ≤ n0 → ¬ m0 + n0 < m + n; (s)

Proof step 12 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), mx[n0, c0] < i, m < #r mx, c0 < c, c < #c mx, c0 < #c mx, c0 + 1 < #c mx, n0 < #r mx, odd(n0), srowsorted(mx, #r mx, mx), m ≤ n0 + 1, m ≤ n0, ¬ mx[n0, c] < i ⊦

Rule argument

Additional information

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

Proof step 13 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  #c mx = #c mx, #r mx = #r mx, countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n0 < #r mx, c0 + 1 < #c mx, c0 < #c mx, c < #c mx, c0 < c, m < #r mx, mx[n0, c0] < i, odd(n0), m ≤ n0, m ≤ n0 + 1, #r mx ≤ #r mx, ¬ mx[n0, c] < i, ∀ r. r < #r mx → (r < #r mx ⊃ perm(mx[r]r, mx[r]r) ∧ ordered≤((even(r) ⊃ mx[r]r;rev(mx[r]r)));mx[r]r = mx[r]r) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ ¬ n < n; (s) Used terms: mx, #r mx, mx

Proof step 14 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Lemma srowsorted-def

Proof step 15 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), mx[n0, c0] < i, m < #r mx, c0 < c, c < #c mx, c0 < #c mx, c0 + 1 < #c mx, n0 < #r mx, odd(n0), m ≤ n0 + 1, m ≤ n0, ¬ mx[n0, c] < i, ∀ r. r < #r mx → ordered≤((even(r) ⊃ mx[r]r;rev(mx[r]r))) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ perm(x, x); (s) ⊦ m ≤ m; (s)

Proof step 16 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 17:

  countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n0 < #r mx, c0 + 1 < #c mx, c0 < #c mx, c < #c mx, c0 < c, m < #r mx, mx[n0, c0] < i, odd(n0), m ≤ n0, m ≤ n0 + 1, ¬ mx[n0, c] < i, n0 < #r mx → ordered≤((even(n0) ⊃ mx[n0]r;rev(mx[n0]r))) ⊦

Rule argument

Additional information

Used terms: n0

Proof step 17 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), mx[n0, c0] < i, m < #r mx, c0 < c, c < #c mx, c0 < #c mx, c0 + 1 < #c mx, n0 < #r mx, odd(n0), ordered≤(rev(mx[n0]r)), m ≤ n0 + 1, m ≤ n0, ¬ mx[n0, c] < i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ odd(n) → ¬ even(n); (s)

Proof step 18 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ ordered≤(x) ↔ (∀ m, n. m ≤ n ∧ n < # x → ¬ x[n] < x[m])

• Proof step 20:

  countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n0 < #r mx, c0 + 1 < #c mx, c0 < #c mx, c < #c mx, c0 < c, m < #r mx, mx[n0, c0] < i, odd(n0), m ≤ n0, m ≤ n0 + 1, ¬ mx[n0, c] < i, ∀ m, n. m ≤ n ∧ n < # rev(mx[n0]r) → ¬ rev(mx[n0]r)[n] < rev(mx[n0]r)[m] ⊦

Rule argument

Additional information

Used terms: rev(mx[n0]r)

Proof step 19 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), mx[n0, c0] < i, m < #r mx, c0 < c, c < #c mx, c0 < #c mx, c0 + 1 < #c mx, n0 < #r mx, odd(n0), m ≤ n0 + 1, m ≤ n0, ¬ mx[n0, c] < i, ∀ m0, n. m0 ≤ n ∧ n < #c mx → ¬ rev(mx[n0]r)[n] < rev(mx[n0]r)[m0] ⊦

Rule argument

Additional information

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

Proof step 21 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 22:

  countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n0 < #r mx, c0 + 1 < #c mx, c0 < #c mx, c < #c mx, c0 < c, m < #r mx, mx[n0, c0] < i, odd(n0), m ≤ n0, m ≤ n0 + 1, ¬ mx[n0, c] < i, #c mx - c + 1 ≤ #c mx - c0 + 1 ∧ #c mx - c0 + 1 < #c mx → ¬ rev(mx[n0]r)[#c mx - c0 + 1] < rev(mx[n0]r)[#c mx - c + 1] ⊦

Rule argument

Additional information

Used terms: #c mx - c + 1, #c mx - c0 + 1

Proof step 22 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), mx[n0, c0] < i, m < #r mx, c0 < c, c < #c mx, c0 < #c mx, c0 + 1 < #c mx, n0 < #r mx, odd(n0), m ≤ n0 + 1, m ≤ n0, ¬ mx[n0, c] < i, #c mx ≤ (#c mx - c0 + 1) + c + 1 → ¬ rev(mx[n0]r)[#c mx - c0 + 1] < rev(mx[n0]r)[#c mx - c + 1] ⊦

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

Proof step 23 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 24:

  #c mx = n1 + c0 + 1, countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n0 < #r mx, c0 + 1 < #c mx, c0 < #c mx, c < #c mx, c0 < c, m < #r mx, mx[n0, c0] < i, odd(n0), m ≤ n0, m ≤ n0 + 1, c0 + 1 ≤ #c mx, ¬ mx[n0, c] < i, #c mx ≤ n1 + c + 1 → ¬ rev(mx[n0]r)[n1] < rev(mx[n0]r)[#c mx - c + 1] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: #c mx, c0 + 1, n

Proof step 24 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  #c mx = n1 + c0 + 1, countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n1 ≠ 0, c0 < n1 + c, n0 < #r mx, c0 + 1 < #c mx, c0 < #c mx, c < #c mx, c0 < c, m < #r mx, mx[n0, c0] < i, odd(n0), m ≤ n0, m ≤ n0 + 1, c ≤ n1 + c0, #c mx ≤ n1 + c + 1, ¬ mx[n0, c] < i, ¬ rev(mx[n0]r)[n1] < rev(mx[n0]r)[#c mx - c + 1] ⊦

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; (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) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ m + n < m; (s) ⊦ m < m + n ↔ n ≠ 0; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ 1 = m + 1 ↔ m = 0; (s) ⊦ m + 1 ≠ 0; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m + 1 ≤ n ↔ m < n; (s)

Proof step 25 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 26:

  #c mx = n1 + c0 + 1, #c mx = n2 + c + 1, countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n1 ≠ 0, mx[n0, c0] < i, m < #r mx, c0 < c, c < #c mx, c0 < #c mx, c0 + 1 < #c mx, n0 < #r mx, c0 < n1 + c, odd(n0), #c mx ≤ n1 + c + 1, c ≤ n1 + c0, m ≤ n0 + 1, m ≤ n0, c + 1 ≤ #c mx, ¬ mx[n0, c] < i, ¬ rev(mx[n0]r)[n1] < rev(mx[n0]r)[n2] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: #c mx, c + 1, n

Proof step 26 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  #c mx = n2 + c + 1, #c mx = n1 + c0 + 1, n1 + c0 = c + n2, countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n1 ≠ 0, c0 < c + n2, c0 < n2 + c, c0 < n1 + c, n0 < #r mx, c0 < #c mx, c0 < c, m < #r mx, mx[n0, c0] < i, c < #c mx, odd(n0), m ≤ n0, m ≤ n0 + 1, #c mx ≤ n1 + c + 1, ¬ mx[n0, c] < i, ¬ rev(mx[n0]r)[n1] < rev(mx[n0]r)[n2] ⊦

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

Proof step 27 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ n < # a → rev(a)[n] = a[# a - n + 1]

• Proof step 29:

  #c mx = n1 + c0 + 1, #c mx = n2 + c + 1, n1 + c0 = c + n2, countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n1 ≠ 0, c < #c mx, mx[n0, c0] < i, m < #r mx, c0 < c, c0 < #c mx, n0 < #r mx, c0 < n1 + c, c0 < n2 + c, c0 < c + n2, odd(n0), #c mx ≤ n1 + c + 1, m ≤ n0 + 1, m ≤ n0, ¬ n1 < # mx[n0]r, ¬ mx[n0, c] < i, ¬ rev(mx[n0]r)[n1] < rev(mx[n0]r)[n2] ⊦

• Proof step 31:

  #c mx = n1 + c0 + 1, #c mx = n2 + c + 1, n1 + c0 = c + n2, countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n1 ≠ 0, c < #c mx, mx[n0, c0] < i, m < #r mx, c0 < c, c0 < #c mx, n0 < #r mx, c0 < n1 + c, c0 < n2 + c, c0 < c + n2, n1 < # mx[n0]r, odd(n0), #c mx ≤ n1 + c + 1, m ≤ n0 + 1, m ≤ n0, ¬ mx[n0, c] < i, ¬ mx[n0]r[# mx[n0]r - n1 + 1] < rev(mx[n0]r)[n2] ⊦

Rule argument

Additional information

Used terms: mx[n0]r, n1

Proof step 28 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  #c mx = n2 + c + 1, #c mx = n1 + c0 + 1, n1 + c0 = c + n2, countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), c0 < c + n2, c0 < n2 + c, c0 < n1 + c, n0 < #r mx, c0 < #c mx, c0 < c, m < #r mx, mx[n0, c0] < i, c < #c mx, c0 < n1, c < n1, c0 + 1 < n1, odd(n0), m ≤ n0, m ≤ n0 + 1, #c mx ≤ n1 + c + 1, #c mx ≤ n1, ¬ mx[n0, c] < i, ¬ rev(mx[n0]r)[n1] < rev(mx[n0]r)[n2] ⊦

Rule argument

Additional information

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

Proof step 30 from proof rowsorted-biggercol-oddbounded (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 + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n → ¬ n < m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ m + n < m; (s) 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 ≠ 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

Proof step 31 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  #c mx = n1 + c0 + 1, #c mx = n2 + c + 1, n1 + c0 = c + n2, countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n1 ≠ 0, n1 < #c mx, c < #c mx, mx[n0, c0] < i, m < #r mx, c0 < c, c0 < #c mx, n0 < #r mx, c0 < n1 + c, c0 < n2 + c, c0 < c + n2, odd(n0), #c mx ≤ n1 + c + 1, m ≤ n0 + 1, m ≤ n0, n1 ≤ n2 + c, ¬ mx[n0, #c mx - n1 + 1] < rev(mx[n0]r)[n2], ¬ mx[n0, c] < i ⊦

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

Proof step 32 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 33:

  #c mx = n2 + c + 1, #c mx = n1 + c0 + 1, #c mx = n3 + n1 + 1, n1 + c0 = c + n2, countodd(mx[c0]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n1 ≠ 0, c0 < c + n2, c0 < n2 + c, c0 < n1 + c, n0 < #r mx, c0 < #c mx, c0 < c, m < #r mx, mx[n0, c0] < i, c < #c mx, n1 < #c mx, odd(n0), n1 ≤ n2 + c, m ≤ n0, m ≤ n0 + 1, #c mx ≤ n1 + c + 1, n1 + 1 ≤ #c mx, ¬ mx[n0, n3] < rev(mx[n0]r)[n2], ¬ mx[n0, c] < i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: #c mx, n1 + 1, n

Proof step 33 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  #c mx = n3 + n1 + 1, #c mx = n2 + c + 1, n1 + n3 = c + n2, countodd(mx[n3]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n1 ≠ 0, n3 < c + n2, rev(mx[n0]r)[n2] < i, c < #c mx, mx[n0, n3] < i, m < #r mx, n3 < c, n3 < #c mx, n0 < #r mx, n3 < n1 + c, n1 < #c mx, odd(n0), #c mx ≤ n1 + c + 1, m ≤ n0 + 1, m ≤ n0, n1 ≤ c + n2, ¬ mx[n0, n3] < rev(mx[n0]r)[n2], ¬ mx[n0, c] < 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; (s) ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m < n → ¬ n < m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ m + n < m; (s) ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) ⊦ m +1 = m + 1; (s) nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification oelem lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic ⊦ m < n ↔ ¬ n ≤ m; (ss) eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic ⊦ m + 1 ≤ n ↔ m < n; (s)

Proof step 34 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ n < # a → rev(a)[n] = a[# a - n + 1]

• Proof step 36:

  #c mx = n2 + c + 1, #c mx = n3 + n1 + 1, n1 + n3 = c + n2, countodd(mx[n3]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n1 ≠ 0, n1 < #c mx, n3 < n1 + c, n0 < #r mx, n3 < #c mx, n3 < c, m < #r mx, mx[n0, n3] < i, c < #c mx, rev(mx[n0]r)[n2] < i, n3 < c + n2, odd(n0), n1 ≤ c + n2, m ≤ n0, m ≤ n0 + 1, #c mx ≤ n1 + c + 1, ¬ n2 < # mx[n0]r, ¬ mx[n0, n3] < rev(mx[n0]r)[n2], ¬ mx[n0, c] < i ⊦

• Proof step 38:

  #c mx = n2 + c + 1, #c mx = n3 + n1 + 1, n1 + n3 = c + n2, countodd(mx[n3]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n1 ≠ 0, n1 < #c mx, n3 < n1 + c, n0 < #r mx, n3 < #c mx, n3 < c, m < #r mx, mx[n0, n3] < i, c < #c mx, mx[n0]r[# mx[n0]r - n2 + 1] < i, n3 < c + n2, n2 < # mx[n0]r, odd(n0), n1 ≤ c + n2, m ≤ n0, m ≤ n0 + 1, #c mx ≤ n1 + c + 1, ¬ mx[n0, n3] < mx[n0]r[# mx[n0]r - n2 + 1], ¬ mx[n0, c] < i ⊦

Rule argument

Additional information

Used terms: mx[n0]r, n2

Proof step 35 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  #c mx = n3 + n1 + 1, #c mx = n2 + c + 1, n1 + n3 = c + n2, countodd(mx[n3]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n1 ≠ 0, n3 < c + n2, rev(mx[n0]r)[n2] < i, c < #c mx, mx[n0, n3] < i, m < #r mx, n3 < c, n3 < #c mx, n0 < #r mx, n3 < n1 + c, n1 < #c mx, c < n2, n3 < n2, n1 < n2, n3 + 1 < n2, odd(n0), #c mx ≤ n1 + c + 1, m ≤ n0 + 1, m ≤ n0, n1 ≤ c + n2, #c mx ≤ n2, ¬ mx[n0, n3] < rev(mx[n0]r)[n2], ¬ mx[n0, c] < i ⊦

Rule argument

Additional information

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

Proof step 37 from proof rowsorted-biggercol-oddbounded (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 + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m < n → m ≤ n; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ m + n < m; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m + m0 < n → ¬ n + n0 < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 38 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  #c mx = n3 + n1 + 1, #c mx = n2 + c + 1, n1 + n3 = c + n2, countodd(mx[n3]c, m, n0, λ j. j < i) = count(mx[c]c, m, n0, λ j. j < i), n1 ≠ 0, c < #c mx, mx[n0, n3] < i, m < #r mx, n3 < c, n3 < #c mx, n0 < #r mx, n3 < n1 + c, n1 < #c mx, n2 < #c mx, n3 < c + n2, mx[n0, #c mx - n2 + 1] < i, odd(n0), n2 ≤ n1 + c, #c mx ≤ n1 + c + 1, m ≤ n0 + 1, m ≤ n0, n1 ≤ c + n2, ¬ mx[n0, c] < i, ¬ mx[n0, n3] < mx[n0, #c mx - n2 + 1] ⊦

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) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ m + n < m; (s) nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification oelem fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat 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 39 from proof rowsorted-biggercol-oddbounded (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification oelem ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: #c mx, n2 + 1, n