Proof step 1 from proof scolsorted-clean0notls (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, #c mx ≠ 0, #clean0rows(mx, i) < #clean0rows(mx0, i), scolsorted(mx, #c mx0, mx0) ⊦

Rule argument

Additional information

Proof step 2 from proof scolsorted-clean0notls (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, #c mx0 ≠ 0, #clean0rows(mx, i) < #clean0rows(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-clean0notls (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

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

Rule argument

Additional information

Used terms: i, mx0

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

Lemma clean0rows-bounded

Proof step 5 from proof scolsorted-clean0notls (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, #c mx0 ≠ 0, #clean0rows(mx, i) < #clean0rows(mx0, i), #clean0rows(mx, i) < #r mx0, scolsorted(mx, #c mx0, mx0), #clean0rows(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-clean0notls (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

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

Rule argument

Additional information

Used terms: mx, i

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

Lemma clean0rows-notallls

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

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[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0, #clean0rows(mx, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i), scolsorted(mx, #c mx0, mx0), #clean0rows(mx0, i) ≤ #r mx0 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

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

Rule argument

Additional information

Used terms: mx[#clean0rows(mx, i)]r, λ j. ¬ j < i

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

A spec-lemma

Proof step 11 from proof scolsorted-clean0notls (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  #c mx = #c mx0, #r mx = #r mx0, n < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i), #clean0rows(mx, i) < #r mx0, scolsorted(mx, #c mx0, mx0), #clean0rows(mx0, i) ≤ #r mx0, ¬ mx[#clean0rows(mx, i), n] < 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 ⊦ mx[r]r[c] = mx[r, c]; (s) ⊦ # mx[r]r = #c mx; (s)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

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

Rule argument

Additional information

Used terms: n, mx0, #clean0rows(mx, i), i

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

Lemma count0-leq-clean0-ind

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

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

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 16:

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

• Proof step 17:

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

Rule argument

Additional information

Used simplifier rules: ⊦ # mx[c]c = #r mx; (s) ⊦ m < n → m ≤ n; (s) Used terms: #clean0rows(mx, i), mx0[n]c, λ j. j < i

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ 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 20:

  #c mx = #c mx0, #r mx = #r mx0, count(mx0[n]c, 0, #clean0rows(mx, i), λ j. j < i) = #clean0rows(mx, i), #clean0rows(mx, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i), n < #c mx0, #clean0rows(mx0, i) ≤ #r mx0, #c mx0 ≤ #c mx, ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx → (c < #c mx0 ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c) ⊦ ∃ m. m < #clean0rows(mx, i) ∧ ¬ mx0[m, n] < i

Rule argument

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

Lemma scolsorted-def

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  #c mx = #c mx0, #r mx = #r mx0, count(mx0[n]c, 0, #clean0rows(mx, i), λ j. j < i) = #clean0rows(mx, i), #clean0rows(mx, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i), n < #c mx0, #clean0rows(mx0, i) ≤ #r mx0, ¬ mx[#clean0rows(mx, i), n] < i, ∀ c. c < #c mx0 → perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c) ⊦ ∃ m. m < #clean0rows(mx, i) ∧ ¬ mx0[m, n] < i

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat

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

User applied rule all left

And obtained the following new goals

• Proof step 22:

  #c mx = #c mx0, #r mx = #r mx0, count(mx0[n]c, 0, #clean0rows(mx, i), λ j. j < i) = #clean0rows(mx, i), n < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i), #clean0rows(mx, i) < #r mx0, #clean0rows(mx0, i) ≤ #r mx0, ¬ mx[#clean0rows(mx, i), n] < i, n < #c mx0 → perm(mx0[n]c, mx[n]c) ∧ ordered≤(mx[n]c) ⊦ ∃ m. m < #clean0rows(mx, i) ∧ ¬ mx0[m, n] < i

Rule argument

Additional information

Used terms: n

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Proof step 23 from proof scolsorted-clean0notls (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ a ∈ y ∧ ¬ a ∈ x → ¬ perm(x, y)

• Proof step 25:

  #c mx = #c mx0, #r mx = #r mx0, count(mx0[n]c, 0, #clean0rows(mx, i), λ j. j < i) = #clean0rows(mx, i), n < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i), #clean0rows(mx, i) < #r mx0, ordered≤(mx[n]c), perm(mx0[n]c, mx[n]c), #clean0rows(mx0, i) ≤ #r mx0, ¬ mx[#clean0rows(mx, i), n] < i ⊦ ∃ m. m < #clean0rows(mx, i) ∧ ¬ mx0[m, n] < i, mx[#clean0rows(mx, i), n] ∈ mx[n]c ∧ ¬ mx[#clean0rows(mx, i), n] ∈ mx0[n]c

Rule argument

Additional information

Used terms: mx0[n]c, mx[n]c, mx[#clean0rows(mx, i), n]

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

A spec-lemma

Proof step 25 from proof scolsorted-clean0notls (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 26:

  #c mx = #c mx0, #r mx = #r mx0, count(mx0[n]c, 0, #clean0rows(mx, i), λ j. j < i) = #clean0rows(mx, i), #clean0rows(mx, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i), n < #c mx0, ordered≤(mx[n]c), perm(mx0[n]c, mx[n]c), #clean0rows(mx0, i) ≤ #r mx0, ¬ mx[#clean0rows(mx, i), n] < i, ¬ mx[#clean0rows(mx, i), n] ∈ mx[n]c ⊦ ∃ m. m < #clean0rows(mx, i) ∧ ¬ mx0[m, n] < i

• Proof step 30:

  #c mx = #c mx0, #r mx = #r mx0, count(mx0[n]c, 0, #clean0rows(mx, i), λ j. j < i) = #clean0rows(mx, i), #clean0rows(mx, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i), n < #c mx0, ordered≤(mx[n]c), perm(mx0[n]c, mx[n]c), mx[#clean0rows(mx, i), n] ∈ mx0[n]c, #clean0rows(mx0, i) ≤ #r mx0, ¬ mx[#clean0rows(mx, i), n] < i ⊦ ∃ m. m < #clean0rows(mx, i) ∧ ¬ mx0[m, n] < i

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 28:

  #c mx = #c mx0, #r mx = #r mx0, count(mx0[n]c, 0, #clean0rows(mx, i), λ j. j < i) = #clean0rows(mx, i), n < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i), #clean0rows(mx, i) < #r mx0, ordered≤(mx[n]c), perm(mx0[n]c, mx[n]c), #clean0rows(mx0, i) ≤ #r mx0, ¬ mx[#clean0rows(mx, i), n] < i, ∀ n0. ¬(n0 < # mx[n]c ∧ mx[n]c[n0] = mx[#clean0rows(mx, i), n]) ⊦ ∃ m. m < #clean0rows(mx, i) ∧ ¬ mx0[m, n] < i

Rule argument

Additional information

Used terms: mx[#clean0rows(mx, i), n], mx[n]c

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

A spec-lemma

Proof step 28 from proof scolsorted-clean0notls (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  #c mx = #c mx0, #r mx = #r mx0, count(mx0[n]c, 0, #clean0rows(mx, i), λ j. j < i) = #clean0rows(mx, i), #clean0rows(mx, i) < #r mx0, #clean0rows(mx, i) < #clean0rows(mx0, i), n < #c mx0, ordered≤(mx[n]c), perm(mx0[n]c, mx[n]c), #clean0rows(mx0, i) ≤ #r mx0, ¬ mx[#clean0rows(mx, i), n] < i, ∀ n0. ¬ n0 < #r mx0 ∨ mx[n0, n] ≠ mx[#clean0rows(mx, i), n] ⊦ ∃ m. m < #clean0rows(mx, i) ∧ ¬ mx0[m, n] < i

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: #clean0rows(mx, i)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 32:

  #c mx = #c mx0, #r mx = #r mx0, count(mx0[n]c, 0, #clean0rows(mx, i), λ j. j < i) = #clean0rows(mx, i), n < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i), #clean0rows(mx, i) < #r mx0, ordered≤(mx[n]c), perm(mx0[n]c, mx[n]c), #clean0rows(mx0, i) ≤ #r mx0, ¬ mx[#clean0rows(mx, i), n] < i, ∃ n0. n0 < # mx0[n]c ∧ mx0[n]c[n0] = mx[#clean0rows(mx, i), n] ⊦ ∃ m. m < #clean0rows(mx, i) ∧ ¬ mx0[m, n] < i

Rule argument

Additional information

Used terms: mx[#clean0rows(mx, i), n], mx0[n]c

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  #c mx = #c mx0, #r mx = #r mx0, mx0[n0, n] = mx[#clean0rows(mx, i), n], count(mx0[n]c, 0, #clean0rows(mx, i), λ j. j < i) = #clean0rows(mx, i), n0 < #r mx0, n < #c mx0, #clean0rows(mx, i) < #clean0rows(mx0, i), #clean0rows(mx, i) < #r mx0, ordered≤(mx[n]c), perm(mx0[n]c, mx[n]c), #clean0rows(mx0, i) ≤ #r mx0, ¬ mx0[n0, n] < i ⊦ ∃ m. m < #clean0rows(mx, i) ∧ ¬ mx0[m, n] < i

Rule argument

Additional information

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

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

User applied rule exists right

And obtained the following new goals

• Proof step 34:

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

Rule argument

Additional information

Used terms: n0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

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

Rule argument

Additional information

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

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 36:

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

• Proof step 37:

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

Rule argument

Additional information

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

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

Lemma sortedperm-count-splits

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

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

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat 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 38 from proof scolsorted-clean0notls (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 39:

  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) Used terms: n, mx0, i

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

Lemma count0-leq-clean0