Proof step 1 from proof scolsorted-count-below-clean0rows (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, count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) ≠ #clean0rows(mx0, i), c < #c mx, scolsorted(mx, #c mx, mx0) ⊦

Rule argument

Additional information

Proof step 2 from proof scolsorted-count-below-clean0rows (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, 0, #clean0rows(mx0, i), λ j. j < i) ≠ #clean0rows(mx0, i), c < #c mx0, scolsorted(mx, #c mx0, 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

Proof step 3 from proof scolsorted-count-below-clean0rows (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

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

Rule argument

Additional information

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

Proof step 4 from proof scolsorted-count-below-clean0rows (previous step) (back to tree)

Lemma scolsorted-clean0notls

Proof step 5 from proof scolsorted-count-below-clean0rows (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[c]c, 0, #clean0rows(mx0, i), λ j. j < i) ≠ #clean0rows(mx0, i), c < #c mx0, scolsorted(mx, #c mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i) ⊦

Rule argument

Additional information

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

Proof step 6 from proof scolsorted-count-below-clean0rows (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

  n ≤ # x ⊦ count(x, 0, n, p) < n ↔ (∃ m. m < n ∧ ¬ p(x[m]))

• Proof step 8:

  #c mx = #c mx0, #r mx = #r mx0, count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) ≠ #clean0rows(mx0, i), c < #c mx0, scolsorted(mx, #c mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) < #clean0rows(mx0, i) ↔ (∃ m. m < #clean0rows(mx0, i) ∧ ¬ mx[c]c[m] < i) ⊦

Rule argument

Additional information

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

Proof step 7 from proof scolsorted-count-below-clean0rows (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof scolsorted-count-below-clean0rows (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  #c mx = #c mx0, #r mx = #r mx0, count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) ≠ #clean0rows(mx0, i), c < #c mx0, scolsorted(mx, #c mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ #clean0rows(mx0, i) - 0 < count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i), count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) < #clean0rows(mx0, i) ↔ (∃ m. m < #clean0rows(mx0, i) ∧ ¬ mx[c]c[m] < i) ⊦

Rule argument

Additional information

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

Proof step 9 from proof scolsorted-count-below-clean0rows (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof scolsorted-count-below-clean0rows (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(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) ≠ #clean0rows(mx0, i), c < #c mx0, count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) < #clean0rows(mx0, i), m < #clean0rows(mx0, i), count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) < #clean0rows(mx, i), m < #clean0rows(mx, i), scolsorted(mx, #c mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[m, c] < 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 ⊦ mx[c]c[r] = mx[r, c]; (s) ⊦ m ≠ n → (m < n ↔ ¬ n < m); (ss) ⊦ m - 0 = m; (s)

Proof step 11 from proof scolsorted-count-below-clean0rows (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  #c mx = #c mx0, #r mx = #r mx0, mx[c]c[m] < i ↔ m < count(mx[c]c, λ j. j < i), count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) ≠ #clean0rows(mx0, i), m < #clean0rows(mx, i), count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) < #clean0rows(mx, i), m < #clean0rows(mx0, i), count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) < #clean0rows(mx0, i), c < #c mx0, scolsorted(mx, #c mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), ¬ mx[m, c] < i ⊦

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

Proof step 12 from proof scolsorted-count-below-clean0rows (previous step) (back to tree)

Lemma sortedperm-count-splits

Proof step 13 from proof scolsorted-count-below-clean0rows (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  #c mx = #c mx0, #r mx = #r mx0, count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) ≠ #clean0rows(mx0, i), c < #c mx0, count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) < #clean0rows(mx0, i), m < #clean0rows(mx0, i), count(mx[c]c, 0, #clean0rows(mx0, i), λ j. j < i) < #clean0rows(mx, i), m < #clean0rows(mx, i), count(mx[c]c, λ j. j < i) < #clean0rows(mx0, i), count(mx[c]c, λ j. j < i) < #clean0rows(mx, i), scolsorted(mx, #c mx0, mx0), #clean0rows(mx0, i) ≤ #clean0rows(mx, i), count(mx[c]c, λ j. j < i) ≤ m, ¬ mx[m, c] < i ⊦

Rule argument

Additional information

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

Proof step 14 from proof scolsorted-count-below-clean0rows (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ ¬ n < n; (s) Used terms: i, mx, c

Proof step 15 from proof scolsorted-count-below-clean0rows (previous step) (back to tree)

Lemma count0-leq-clean0