Proof step 1 from proof scolsorted-clean1notls (conclusion) (back to tree)

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

System applied rule normalize

And obtained the following new goals

Proof step 2:
#c mx = #c mx0, #r mx = #r mx0, #c mx ≠ 0, #clean1rows(mx, i) < #clean1rows(mx0, i), scolsorted(mx, #c mx0, mx0) ⊦

Rule argument

Additional information

Proof step 2 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx = #r mx0, #c mx ≠ 0, #clean1rows(mx, i) < #clean1rows(mx0, i), scolsorted(mx, #c mx0, mx0) ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 3:
#c mx = #c mx0, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx, i) < #clean1rows(mx0, i), scolsorted(mx, #c mx0, mx0) ⊦

Rule argument

Additional information

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

Proof step 3 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx, i) < #clean1rows(mx0, i), scolsorted(mx, #c mx0, mx0) ⊦

User applied rule apply lemma

And obtained the following new goals

Proof step 4:
⊦ ¬ #r mx < #clean1rows(mx, i)
Proof step 5:
#c mx = #c mx0, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx, i) < #clean1rows(mx0, i), scolsorted(mx, #c mx0, mx0), ¬ #r mx0 < #clean1rows(mx0, i) ⊦

Rule argument

spec: <toplevel>, name:clean1rows-bounded, seq: ⊦ ¬ #r mx < #clean1rows(mx, i), subst:[i, mx] → [i, mx0]

Additional information

Used terms: i, mx0

Proof step 4 from proof scolsorted-clean1notls (previous step) (back to tree)

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

Lemma clean1rows-bounded

Proof step 5 from proof scolsorted-clean1notls (previous step) (back to tree)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 6:
#c mx = #c mx0, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0 ⊦

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: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 6 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0 ⊦

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:
#c mx = #c mx0, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #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 ⊦

Rule argument

spec: <toplevel>, name:clean1rows-notallge, seq:⊦ #clean1rows(mx, i) + r + 1 = #r mx → count(mx[r]r, λ j. j < i) ≠ 0, subst:[mx, i, r] → [mx, i, #r mx - #clean1rows(mx, i) + 1]

Additional information

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

Proof step 7 from proof scolsorted-clean1notls (previous step) (back to tree)

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

Lemma clean1rows-notallge

Proof step 8 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #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 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 9:
#c mx = #c mx0, #r mx = #r mx0, #c mx0 ≠ 0, count(mx[#r mx0 - #clean1rows(mx, i) + 1]r, λ j. j < i) ≠ 0, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0 ⊦

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

Proof step 9 from proof scolsorted-clean1notls (previous step) (back to tree)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

Proof step 10:
#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #c mx0 ≠ 0, count(mx[n0]r, λ j. j < i) ≠ 0, #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx, i) + 1 ≤ #r mx0 ⊦

Rule argument

spec: nat, name:elim-sub, seq:n ≤ m ⊦ n0 = m - n ↔ m = n0 + n, subst:[m, n, n0] → [#r mx0, #clean1rows(mx, i) + 1, n0]

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: #r mx0, #clean1rows(mx, i) + 1, n0

Proof step 10 from proof scolsorted-clean1notls (previous step) (back to tree)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 11:
#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #c mx0 ≠ 0, count(mx[n0]r, λ j. j < i) ≠ 0, #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0 ⊦

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

Proof step 11 from proof scolsorted-clean1notls (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:
#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, ∃ n. ¬(n < # mx[n0]r → ¬ mx[n0]r[n] < i) ⊦

Rule argument

spec: filter-count[oarray-sort-new], name:count-zero, seq: ⊦ count(x, p) = 0 ↔ (∀ n. n < # x → ¬ p(x[n])), subst:[x, p] → [mx[n0]r, λ j. j < i], <all paths>

Additional information

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

Proof step 12 from proof scolsorted-clean1notls (previous step) (back to tree)

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

A spec-lemma

Proof step 13 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, ∃ n. ¬(n < # mx[n0]r → ¬ mx[n0]r[n] < i) ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 14:
#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0 ⊦

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 ⊦ # mx[r]r = #c mx; (s) ⊦ mx[r]r[c] = mx[r, c]; (s)

Proof step 14 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0 ⊦

User applied rule apply lemma

And obtained the following new goals

Proof step 15:
c < #c mx ⊦ #clean1rows(mx, i) ≤ count(mx[c]c, λ j. ¬ j < i)
Proof step 16:
#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx0[n]c, λ j. ¬ j < i) ⊦

Rule argument

spec: <toplevel>, name:count1-leq-clean1, seq:c < #c mx ⊦ #clean1rows(mx, i) ≤ count(mx[c]c, λ j. ¬ j < i), subst:[c, mx, i] → [n, mx0, i]

Additional information

Used terms: n, mx0, i

Proof step 15 from proof scolsorted-clean1notls (previous step) (back to tree)

c < #c mx ⊦ #clean1rows(mx, i) ≤ count(mx[c]c, λ j. ¬ j < i)

Lemma count1-leq-clean1

Proof step 16 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx0[n]c, λ j. ¬ j < i) ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 17:
#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < count(mx0[n]c, λ j. ¬ j < i), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx0[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦

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

Proof step 17 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < count(mx0[n]c, λ j. ¬ j < i), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx0[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 18:
⊦ perm(x, y) → count(x, p) = count(y, p)
Proof step 19:
#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i) ⊦

Rule argument

spec: filter-count[oarray-sort-new], name:perm-count, seq: ⊦ perm(x, y) → count(x, p) = count(y, p), subst:[y, x, p] → [mx[n]c, mx0[n]c, λ j. ¬ j < i], <all paths>

Additional information

Used simplifier rules: scolsorted-permcol: #c mx = #c mx0, c < #c mx ⊦ scolsorted(mx, #c mx0, mx0) → perm(mx0[c]c, mx[c]c); Used terms: mx[n]c, mx0[n]c, λ j. ¬ j < i

Proof step 18 from proof scolsorted-clean1notls (previous step) (back to tree)

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

A spec-lemma

Proof step 19 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i) ⊦

User applied rule apply lemma

And obtained the following new goals

Proof step 20:
ordered≤(x), n < # x ⊦ n < count(x, λ b. b < a) ↔ x[n] < a
Proof step 21:
#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦ ordered≤(mx[n]c) ∧ n0 < # mx[n]c
Proof step 28:
#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, n0 < count(mx[n]c, λ b. b < i) ↔ mx[n]c[n0] < i, n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦

Rule argument

spec: olist-new[oarray-sort-new], name:ordered-count-splits, seq:ordered≤(x), n < # x ⊦ n < count(x, λ b. b < a) ↔ x[n] < a, subst:[x, n, a] → [mx[n]c, n0, i]

Additional information

Used terms: mx[n]c, n0, i

Proof step 20 from proof scolsorted-clean1notls (previous step) (back to tree)

ordered≤(x), n < # x ⊦ n < count(x, λ b. b < a) ↔ x[n] < a

A spec-lemma

Proof step 21 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦ ordered≤(mx[n]c) ∧ n0 < # mx[n]c

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 22:
#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, #clean1rows(mx, i) < n0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #r mx0 ≤ n0, #clean1rows(mx0, i) ≤ n0 ⊦

Rule argument

Additional information

Used simplifier rules: scolsorted-colordered: #c mx = #c mx0, c < #c mx ⊦ scolsorted(mx, #c mx0, mx0) → ordered≤(mx[c]c); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (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)

Proof step 22 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, #clean1rows(mx, i) < n0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #r mx0 ≤ n0, #clean1rows(mx0, i) ≤ n0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 23:
⊦ 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 24:
#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx, i) < n0, n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, perm(mx0[n]c, mx[n]c), #clean1rows(mx0, i) ≤ n0, #r mx0 ≤ n0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0, #c mx0 ≤ #c mx, ∀ 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

spec: <toplevel>, name:scolsorted-def, seq:⊦ 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 ))), subst:[mx, m, mx0] → [mx, #c mx0, mx0], <all paths>

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 23 from proof scolsorted-clean1notls (previous step) (back to tree)

⊦ 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)))

Lemma scolsorted-def

Proof step 24 from proof scolsorted-clean1notls (previous step) (back to tree)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 25:
#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx, i) < n0, n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, perm(mx0[n]c, mx[n]c), #clean1rows(mx0, i) ≤ n0, #r mx0 ≤ n0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0, ∀ 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 25 from proof scolsorted-clean1notls (previous step) (back to tree)

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

User applied rule all left

And obtained the following new goals

Proof step 26:
#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, #clean1rows(mx, i) < n0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #r mx0 ≤ n0, #clean1rows(mx0, i) ≤ n0, n < #c mx0 → perm(mx0[n]c, mx[n]c) ∧ ordered≤(mx[n]c) ⊦

Rule argument

pos: left 15 terms: n abort: F discard: T computed: T

Additional information

Used terms: n

Proof step 26 from proof scolsorted-clean1notls (previous step) (back to tree)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 27:
#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx, i) < n0, n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, ordered≤(mx[n]c), perm(mx0[n]c, mx[n]c), #clean1rows(mx0, i) ≤ n0, #r mx0 ≤ n0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦

Rule argument

Additional information

Proof step 27 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx, i) < n0, n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, ordered≤(mx[n]c), perm(mx0[n]c, mx[n]c), #clean1rows(mx0, i) ≤ n0, #r mx0 ≤ n0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦

User applied rule subst equation

And closed the goal!

Rule argument

pos: left 2, flags: discard

Additional information

Used simplifier rules: ⊦ 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 28 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, n0 < count(mx[n]c, λ b. b < i) ↔ mx[n]c[n0] < i, n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 29:
#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), n0 < count(mx[n]c, λ b. b < i), n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦

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 ⊦ mx[c]c[r] = mx[r, c]; (s)

Proof step 29 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), n0 < count(mx[n]c, λ b. b < i), n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦

User applied rule apply lemma

And obtained the following new goals

Proof step 30:
∀ n. n < # x → ¬(p(x[n]) ∧ p0(x[n])) ⊦ count(x, p) + count(x, p0) = count(x, λ a. p(a) ∨ p0(a))
Proof step 31:
#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = count(mx[n]c, λ i0. i0 < i ∨ ¬ i0 < i), #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, n0 < count(mx[n]c, λ b. b < i), #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i) ⊦

Rule argument

spec: filter-count[oarray-sort-new], name:count-add-dis, seq:∀ n. n < # x → ¬(p(x[n]) ∧ p0(x[n])) ⊦ count(x, p) + count(x, p0) = count(x, λ a. p(a) ∨ p0(a)), subst:[x, p, p0] → [mx[n]c, λ j. j < i, λ j. ¬ j < i]

Additional information

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

Proof step 30 from proof scolsorted-clean1notls (previous step) (back to tree)

∀ n. n < # x → ¬(p(x[n]) ∧ p0(x[n])) ⊦ count(x, p) + count(x, p0) = count(x, λ a. p(a) ∨ p0(a))

A spec-lemma

Proof step 31 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = count(mx[n]c, λ i0. i0 < i ∨ ¬ i0 < i), #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, n0 < count(mx[n]c, λ b. b < i), #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i) ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 32:
#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = count(mx[n]c, λ i0. true), #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), n0 < count(mx[n]c, λ b. b < i), n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦

Rule argument

Additional information

Proof step 32 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = count(mx[n]c, λ i0. true), #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), n0 < count(mx[n]c, λ b. b < i), n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 33:
⊦ count(x, p) = count(x, 0, # x, p)
Proof step 34:
#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = count(mx[n]c, 0, # mx[n]c, λ i0. true), #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, n0 < count(mx[n]c, λ b. b < i), #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i) ⊦

Rule argument

spec: filter-count[oarray-sort-new], name:count-def, seq: ⊦ count(x, p) = count(x, 0, # x, p), subst:[x, p] → [mx[n]c, λ i0. true], <all paths>

Additional information

Used terms: mx[n]c, λ i0. true

Proof step 33 from proof scolsorted-clean1notls (previous step) (back to tree)

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

A spec-lemma

Proof step 34 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = count(mx[n]c, 0, # mx[n]c, λ i0. true), #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, n0 < count(mx[n]c, λ b. b < i), #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i) ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 35:
#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = count(mx[n]c, 0, #r mx0, λ i0. true), #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), n0 < count(mx[n]c, λ b. b < i), n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦

Rule argument

Additional information

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

Proof step 35 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = count(mx[n]c, 0, #r mx0, λ i0. true), #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), n0 < count(mx[n]c, λ b. b < i), n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #clean1rows(mx0, i) ≤ #r mx0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 36:
m ≤ # x ⊦ count(x, 0, m, λ a. true) = m
Proof step 37:
#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = #r mx0, #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, n0 < count(mx[n]c, λ b. b < i), #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #r mx0 ≤ # mx[n]c ⊦

Rule argument

spec: filter-count[oarray-sort-new], name:count-true, seq:m ≤ # x ⊦ count(x, 0, m, λ a. true) = m, subst:[x, m] → [mx[n]c, #r mx0], <all paths>

Additional information

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

Proof step 36 from proof scolsorted-clean1notls (previous step) (back to tree)

m ≤ # x ⊦ count(x, 0, m, λ a. true) = m

A spec-lemma

Proof step 37 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = #r mx0, #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, n0 < count(mx[n]c, λ b. b < i), #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), #r mx0 ≤ # mx[n]c ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 38:
#c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = #r mx0, #clean1rows(mx, i) < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), mx[n0, n] < i, n < #c mx0, n0 < count(mx[n]c, λ b. b < i), #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ #r mx0, #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i) ⊦

Rule argument

Additional information

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

Proof step 38 from proof scolsorted-clean1notls (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 39:
⊦ m ≤ n ↔ (∃ n0. m + n0 = n)
Proof step 40:
#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), n0 < count(mx[n]c, λ b. b < i), n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), ∃ n0. #clean1rows(mx0, i) + n0 = #r mx0 ⊦

Rule argument

spec: nat, name:le-addex, seq: ⊦ m ≤ n ↔ (∃ n0. m + n0 = n), subst:[m, n] → [#clean1rows(mx0, i), #r mx0], <all paths>

Additional information

Used terms: #clean1rows(mx0, i), #r mx0

Proof step 39 from proof scolsorted-clean1notls (previous step) (back to tree)

⊦ m ≤ n ↔ (∃ n0. m + n0 = n)

A spec-lemma

Proof step 40 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), n0 < count(mx[n]c, λ b. b < i), n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i), ∃ n0. #clean1rows(mx0, i) + n0 = #r mx0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 41:
#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = #r mx0, #clean1rows(mx0, i) + n1 = #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), n0 < count(mx[n]c, λ b. b < i), n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i) ⊦

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic

Proof step 41 from proof scolsorted-clean1notls (previous step) (back to tree)

#c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx, i) + 1, #r mx = #r mx0, count(mx[n]c, λ j. j < i) + count(mx[n]c, λ j. ¬ j < i) = #r mx0, #clean1rows(mx0, i) + n1 = #r mx0, #clean1rows(mx, i) < count(mx[n]c, λ j. ¬ j < i), n0 < count(mx[n]c, λ b. b < i), n < #c mx0, mx[n0, n] < i, #clean1rows(mx, i) < #clean1rows(mx0, i), #clean1rows(mx, i) < #r mx0, perm(mx0[n]c, mx[n]c), scolsorted(mx, #c mx0, mx0), #clean1rows(mx0, i) ≤ count(mx[n]c, λ j. ¬ j < i) ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 42:
⊦ m < n ↔ (∃ m0. m + m0 = n ∧ m0 ≠ 0)

Rule argument

spec: nat-basic, name:addex, seq: ⊦ m < n ↔ (∃ m0. m + m0 = n ∧ m0 ≠ 0), subst:[m, n] → [n0, count(mx[n]c, λ j. j < i)], <all paths>

Additional information

Used simplifier rules: eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat ⊦ m + m0 ≤ m ↔ m0 = 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: n0, count(mx[n]c, λ j. j < i)