Proof step 1 from proof scolsort-dirtyboundhalf (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  #c mx0 = #c mx, #r mx0 = #r mx, #c mx ≠ 0, mx0.dirtyrows≤(bound), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx0, mx0), ¬ mx.dirtyrows≤(bound /↑ 2) ⊦

Rule argument

Additional information

Proof step 2 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ mx.dirtyrows≤(bound) ↔ (∀ i. #dirtyrows(mx, i) ≤ bound)

• Proof step 4:

  #c mx0 = #c mx, #r mx0 = #r mx, #c mx ≠ 0, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx0, mx0), ¬ mx.dirtyrows≤(bound /↑ 2), ∀ i. #dirtyrows(mx0, i) ≤ bound ⊦

Rule argument

Additional information

Used terms: mx0, bound

Proof step 3 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma dirtyrowsbound-def

Proof step 4 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  #c mx0 = #c mx, #r mx0 = #r mx, #c mx ≠ 0, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), ¬ mx.dirtyrows≤(bound /↑ 2), ∀ i. #dirtyrows(mx0, i) ≤ bound ⊦

Rule argument

Additional information

Proof step 5 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ mx.dirtyrows≤(bound) ↔ (∀ i. #dirtyrows(mx, i) ≤ bound)

• Proof step 7:

  #c mx0 = #c mx, #r mx0 = #r mx, #c mx ≠ 0, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), ∀ i. #dirtyrows(mx0, i) ≤ bound, ∃ i. ¬ #dirtyrows(mx, i) ≤ bound /↑ 2 ⊦

Rule argument

Additional information

Used terms: mx, bound /↑ 2

Proof step 6 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma dirtyrowsbound-def

Proof step 7 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  #c mx0 = #c mx, #r mx0 = #r mx, #c mx ≠ 0, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), ∀ i. #dirtyrows(mx0, i) ≤ bound ⊦

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; (ss)

Proof step 8 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 9:

  #c mx0 = #c mx, #r mx0 = #r mx, #c mx ≠ 0, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound ⊦

Rule argument

Additional information

Used terms: i

Proof step 9 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 10:

  ⊦ #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx

• Proof step 11:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound ⊦

Rule argument

Additional information

Used terms: i, mx

Proof step 10 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma dirtyrows-def

Proof step 11 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 12:

  ⊦ #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx

• Proof step 13:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #c mx ≠ 0, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound ⊦

Rule argument

Additional information

Used terms: i, mx0

Proof step 12 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma dirtyrows-def

Proof step 13 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound ⊦

Rule argument

Additional information

Proof step 14 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 15:

  #c mx ≠ 0 ⊦ ∃ c. c < #c mx ∧ (∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i))

• Proof step 16:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #c mx ≠ 0, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, ∃ c. c < #c mx ∧ (∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i)) ⊦

Rule argument

Additional information

Used terms: mx, i

Proof step 15 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma exists-max0column

Proof step 16 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, bound /↑ 2 < #dirtyrows(mx, i), c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 17 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦ #r mx = #r mx0 ∧ #c mx = #c mx0 ∧ srowsorted(mx0, #r mx0, mx0) ∧ (∀ c1. c1 < #c mx → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i))

• Proof step 21:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, #clean0rows(mx, i) ≥ #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: mx, mx0, c, i

Proof step 18 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma max0column-clean0rowsbounded

Proof step 19 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, count(mx[c]c, λ j. j < i) < count(mx[c1]c, λ j. j < i), c1 < #c mx, bound /↑ 2 < #dirtyrows(mx, i), c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 20 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: c1

Proof step 21 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, bound /↑ 2 < #dirtyrows(mx, i), c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n ≥ m ↔ m ≤ n; (s)

Proof step 22 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 23:

  c0 < #c mx, ∀ c. c < #c mx → ordered≤(mx[c]c), ∀ c. c < #c mx → count(mx[c]c, λ j. j < i) ≤ count(mx[c0]c, λ j. j < i) ⊦ #clean1rows(mx, i) + count(mx[c0]c, λ j. j < i) = #r mx

• Proof step 24:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #dirtyrows(mx0, i) ≤ bound, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦ (∀ c. c < #c mx → ordered≤(mx[c]c)) ∧ (∀ c1. c1 < #c mx → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i))

• Proof step 32:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #clean1rows(mx, i) + count(mx[c]c, λ j. j < i) = #r mx, c < #c mx, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #dirtyrows(mx0, i) ≤ bound, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: c, mx, i

Proof step 23 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma max0column-determines-clean1rows

Proof step 24 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, bound /↑ 2 < #dirtyrows(mx, i), c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦ (c0 < #c mx → ordered≤(mx[c0]c)) ∧ (c1 < #c mx → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i))

Rule argument

Additional information

Proof step 25 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 26:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c0 < #c mx, c < #c mx, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #dirtyrows(mx0, i) ≤ bound, ¬ ordered≤(mx[c0]c), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

• Proof step 30:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c1 < #c mx, c < #c mx, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #dirtyrows(mx0, i) ≤ bound, ¬ count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

Proof step 26 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, bound /↑ 2 < #dirtyrows(mx, i), c < #c mx, c0 < #c mx, srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #c mx ≤ #c mx, ¬ ordered≤(mx[c0]c), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i), ∀ c. c < #c mx → (c < #c mx ⊃ perm(mx0[c]c, mx[c]c) ∧ ordered≤(mx[c]c);mx0[c]c = mx[c]c) ⊦

Rule argument

Additional information

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

Proof step 27 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma scolsorted-def

Proof step 28 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, bound /↑ 2 < #dirtyrows(mx, i), c < #c mx, c0 < #c mx, srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), ¬ ordered≤(mx[c0]c), ∀ c1. c1 < #c mx → perm(mx0[c1]c, mx[c1]c) ∧ ordered≤(mx[c1]c), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 29 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: c0

Proof step 30 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, count(mx[c]c, λ j. j < i) < count(mx[c1]c, λ j. j < i), c1 < #c mx, c < #c mx, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #dirtyrows(mx0, i) ≤ bound, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss)

Proof step 31 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: c1

Proof step 32 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, bound /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #dirtyrows(mx0, i) ≤ bound, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, 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 eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic

Proof step 33 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 34:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), bound /↑ 2 < #dirtyrows(mx, i), c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #dirtyrows(mx, i) ≤ #dirtyrows(mx0, i) /↑ 2, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i) ⊦

• Proof step 60:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), bound /↑ 2 < #dirtyrows(mx, i), c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), ¬ #dirtyrows(mx, i) ≤ #dirtyrows(mx0, i) /↑ 2, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i) ⊦

Rule argument

Additional information

Used formulas: #dirtyrows(mx, i) ≤ #dirtyrows(mx0, i) /↑ 2

Proof step 34 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, bound /↑ 2 < #dirtyrows(mx, i), bound /↑ 2 < #dirtyrows(mx0, i) /↑ 2, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx, i) ≤ #dirtyrows(mx0, i) /↑ 2, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #dirtyrows(mx0, i) ≤ bound, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, 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

Proof step 35 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ m /↑ n = (∃ n0. m = n0 * n ⊃ m / n;m / n + 1)

• Proof step 37:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #dirtyrows(mx, i) ≤ #dirtyrows(mx0, i) /↑ 2, (∃ n0. bound = n0 * 2 ⊃ bound / 2;bound / 2 + 1) < #dirtyrows(mx0, i) /↑ 2, (∃ n0. bound = n0 * 2 ⊃ bound / 2;bound / 2 + 1) < #dirtyrows(mx, i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i) ⊦

Rule argument

Additional information

Used terms: bound, 2

Proof step 36 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma divup-def

Proof step 37 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  ⊦ m /↑ n = (∃ n0. m = n0 * n ⊃ m / n;m / n + 1)

• Proof step 39:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #dirtyrows(mx0, i) ≤ bound, (∃ n0. bound = n0 * 2 ⊃ bound / 2;bound / 2 + 1) < #dirtyrows(mx, i), (∃ n0. bound = n0 * 2 ⊃ bound / 2;bound / 2 + 1) < (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), #dirtyrows(mx, i) ≤ (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1) ⊦

Rule argument

Additional information

Used terms: #dirtyrows(mx0, i), 2

Proof step 38 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma divup-def

Proof step 39 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 40:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), (∃ n0. bound = n0 * 2 ⊃ bound / 2;bound / 2 + 1) < #dirtyrows(mx, i), bound / 2 < (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∃ n0. bound = n0 * 2, #dirtyrows(mx, i) ≤ (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1) ⊦

• Proof step 44:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ bound, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), (∃ n0. bound = n0 * 2 ⊃ bound / 2;bound / 2 + 1) < #dirtyrows(mx, i), bound / 2 + 1 < (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ n0. bound ≠ n0 * 2, #dirtyrows(mx, i) ≤ (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1) ⊦

Rule argument

Additional information

Proof step 40 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #dirtyrows(mx0, i) ≤ n0 * 2, n0 < (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1), (∃ n. n0 * 2 = n * 2 ⊃ n0;n0 + 1) < #dirtyrows(mx, i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), #dirtyrows(mx, i) ≤ (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1) ⊦

Rule argument

Additional information

Used simplifier rules: mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ (2 * m) / 2 = m; (s)

Proof step 41 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 42:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), c < #c mx, n0 < #dirtyrows(mx0, i) / 2 + 1, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx0, i) ≤ n0 * 2, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), (∃ n. n0 * 2 = n * 2 ⊃ n0;n0 + 1) < #dirtyrows(mx, i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2, #dirtyrows(mx, i) ≤ (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1) ⊦

Rule argument

Additional information

Used simplifier rules: f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ (2 * m) / 2 = m; (s) ⊦ m < n → n ≠ 0; (s) 0 ≠ m ⊦ (* m) * n ≤ m * n0 ↔ n ≤ n0; (s) ⊦ m < n → (n ≤ m ↔ false); (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult

Proof step 42 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n0 * 2, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, n0 * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), (∃ n. n0 * 2 = n * 2 ⊃ n0;n0 + 1) < #dirtyrows(mx, i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2, #dirtyrows(mx, i) ≤ (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ n0;n0 + 1) ⊦

Rule argument

Additional information

Used simplifier rules: mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ (2 * m) / 2 = m; (s) ⊦ m ≤ m; (s) 0 ≠ m ⊦ (* m) * n ≤ m * n0 ↔ n ≤ n0; (s) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) m0 ≠ 0 ⊦ n ≤ m / m0 ↔ n * m0 ≤ m; (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)

Proof step 43 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n0

Proof step 44 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 45:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, bound / 2 + 1 < #dirtyrows(mx0, i) / 2, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #dirtyrows(mx0, i) ≤ bound, (∃ n0. bound = n0 * 2 ⊃ bound / 2;bound / 2 + 1) < #dirtyrows(mx, i), ∀ n0. bound ≠ n0 * 2, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∃ n0. #dirtyrows(mx0, i) = n0 * 2, #dirtyrows(mx, i) ≤ (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ #dirtyrows(mx0, i) / 2;#dirtyrows(mx0, i) / 2 + 1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + n < m + n0 ↔ n < n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ls-02: n ≠ 0 ⊦ m / n < m0 / n → m < m0; (forward) from specification nat-div f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m / 2 = 0 ↔ m = 0 ∨ m = 1; (s) ⊦ m < n → n ≠ 0; (s) ⊦ m ≤ n → (n < m ↔ false); (s)

Proof step 45 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n0 * 2, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, n0 * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), bound / 2 + 1 < n0, c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), n0 * 2 ≤ bound, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), (∃ n0. bound = n0 * 2 ⊃ bound / 2;bound / 2 + 1) < #dirtyrows(mx, i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ n0. bound ≠ n0 * 2, #dirtyrows(mx, i) ≤ (∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊃ n0;n0 + 1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ (2 * m) / 2 = m; (s)

Proof step 46 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 47:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n0 * 2, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), n0 * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, bound / 2 + 1 < n0, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), n0 * 2 ≤ bound, #dirtyrows(mx, i) ≤ n0, (∃ n0. bound = n0 * 2 ⊃ bound / 2;bound / 2 + 1) < #dirtyrows(mx, i), ∀ n0. bound ≠ n0 * 2, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∃ n0. #dirtyrows(mx0, i) = n0 * 2 ⊦

• Proof step 59:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n0 * 2, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), n0 * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, bound / 2 + 1 < n0, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), n0 * 2 ≤ bound, #dirtyrows(mx, i) ≤ n0 + 1, (∃ n0. bound = n0 * 2 ⊃ bound / 2;bound / 2 + 1) < #dirtyrows(mx, i), ∀ n0. bound ≠ n0 * 2, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ n0. #dirtyrows(mx0, i) ≠ n0 * 2 ⊦

Rule argument

Additional information

Proof step 47 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n * 2, #r mx0 = #r mx, n0 * 2 = n * 2, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, n * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), bound / 2 + 1 < n0, c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx, i) ≤ n0, n * 2 ≤ bound, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), (∃ n0. bound = n0 * 2 ⊃ bound / 2;bound / 2 + 1) < #dirtyrows(mx, i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ n0. bound ≠ n0 * 2 ⊦

Rule argument

Additional information

Proof step 48 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 49:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n * 2, #r mx0 = #r mx, n0 * 2 = n * 2, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), n * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, bound / 2 + 1 < n0, bound / 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), n * 2 ≤ bound, #dirtyrows(mx, i) ≤ n0, ∀ n0. bound ≠ n0 * 2, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∃ n0. bound = n0 * 2 ⊦

• Proof step 51:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n * 2, #r mx0 = #r mx, n0 * 2 = n * 2, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), n * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, bound / 2 + 1 < n0, bound / 2 + 1 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), n * 2 ≤ bound, #dirtyrows(mx, i) ≤ n0, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ n0. bound ≠ n0 * 2 ⊦

Rule argument

Additional information

Proof step 49 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n * 2, #r mx0 = #r mx, n0 * 2 = n * 2, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), n * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, n1 < n0, n < #dirtyrows(mx, i), n1 + 1 < n0, n1 < #dirtyrows(mx, i), c < #c mx, n < n0, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), n ≤ n1, #dirtyrows(mx, i) ≤ n0, ∀ n0. n1 * 2 ≠ n0 * 2, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i) ⊦

Rule argument

Additional information

Used simplifier rules: fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ (2 * m) / 2 = m; (s) 0 ≠ m ⊦ (* m) * n ≤ m * n0 ↔ n ≤ n0; (s)

Proof step 50 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n1

Proof step 51 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ m0 ≠ 0 → (m * m0 = n * m0 ↔ m = n)

• Proof step 53:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n * 2, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, n * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), n0 = n, 2 ≠ 0, bound / 2 + 1 < #dirtyrows(mx, i), bound / 2 + 1 < n0, c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx, i) ≤ n0, n * 2 ≤ bound, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), ∀ n0. bound ≠ n0 * 2, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i) ⊦

Rule argument

Additional information

Used terms: n0, 2, n

Proof step 52 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

A spec-lemma

Proof step 53 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n * 2, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, n * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), bound / 2 + 1 < #dirtyrows(mx, i), bound / 2 + 1 < n, c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx, i) ≤ n, n * 2 ≤ bound, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), ∀ n0. bound ≠ n0 * 2, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, 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

Proof step 54 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 55:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n * 2, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), n * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, bound = m0 * 2 + n1, 2 ≠ 0, c < #c mx, m0 + 1 < n, m0 + 1 < #dirtyrows(mx, i), n1 < 2, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), n * 2 ≤ bound, #dirtyrows(mx, i) ≤ n, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ n0. bound ≠ n0 * 2 ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n; (elim) Used terms: bound, 2, m0, n1

Proof step 55 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n * 2, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, n * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), n1 < 2, m0 + 1 < #dirtyrows(mx, i), c < #c mx, m0 + 1 < n, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx, i) ≤ n, n * 2 ≤ m0 * 2 + n1, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), ∀ n0. m0 * 2 + n1 ≠ n0 * 2, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i) ⊦

Rule argument

Additional information

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

Proof step 56 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And obtained the following new goals

• Proof step 57:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n * 2, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), n * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, m0 * 2 + n1 ≠ n * 2, m0 + 1 < n, c < #c mx, m0 + 1 < #dirtyrows(mx, i), n1 < 2, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), n * 2 ≤ m0 * 2 + n1, #dirtyrows(mx, i) ≤ n, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ n0. m0 * 2 + n1 ≠ n0 * 2 ⊦

Rule argument

Additional information

Used terms: n

Proof step 57 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  #c mx0 = #c mx, #dirtyrows(mx0, i) = n * 2, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), n * 2 + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, m0 * 2 + n1 ≠ n * 2, n * 2 < m0 * 2 + n1, m0 + 1 < n, c < #c mx, m0 + 1 < #dirtyrows(mx, i), n1 < 2, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #dirtyrows(mx, i) ≤ n, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ n0. m0 * 2 + n1 ≠ n0 * 2 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (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 → (m ≤ n ↔ m < n); (s)

Proof step 58 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; ⊦ m < n + 1 ↔ ¬ n < m; (s) n < n0 ⊦ m + (* n) < (* n0) ↔ m < n0 - n; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m +1 = m + 1; (s) ⊦ n + 0 = n; (s) 0 ≠ m ⊦ (* m) * n ≤ m * n0 ↔ n ≤ n0; (s) ⊦ 2 * m ≠ 2 * n + 1; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ ¬ 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 * n = m * n0 ↔ m = 0 ∨ n = n0; (ws) ⊦ 2 * m < 2 * n ↔ m < n; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat 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 ≠ 0; (s) ⊦ m + m0 < n → ¬ n + n0 < m; (s)

Proof step 59 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n0

Proof step 60 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, bound /↑ 2 < #dirtyrows(mx, i), #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), #dirtyrows(mx0, i) ≤ bound, ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i) ⊦

Rule argument

Additional information

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

Proof step 61 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 62:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i) ⊦

Rule argument

Additional information

Proof step 62 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 63:

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

• Proof step 64:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, c < #c mx, #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i) ⊦ #r mx = #r mx0 ∧ #c mx = #c mx0 ∧ c < #c mx ∧ c < #c mx ∧ scolsorted(mx, #c mx, mx0) ∧ (∀ c1. c1 < #c mx → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i))

• Proof step 66:

  #c mx = #c mx0, #r mx = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) = #clean0rows(mx0, i) + count(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), c < #c mx, scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ c1. c1 < #c mx → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 63 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma max0column-countcol

Proof step 64 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  #c mx0 = #c mx, #r mx0 = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) = count(mx[c]c, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #dirtyrows(mx, i) + #clean0rows(mx, i) < count(mx[c1]c, λ j. j < i), c1 < #c mx, c < #c mx, #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx, mx0), srowsorted(mx0, #r mx, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx, λ j. j < i)) ≤ #clean0rows(mx, i), ∀ c0. c0 < #c mx → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, 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 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 < m; (ss)

Proof step 65 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: c1

Proof step 66 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 67:

  #c mx = #c mx0, #r mx = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) = #clean0rows(mx0, i) + count(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx0, #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), c < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≤ #clean0rows(mx, i), ∀ c0. c0 < #c mx0 → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ c1. c1 < #c mx0 → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 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 67 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 68:

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

• Proof step 69:

  #c mx = #c mx0, #r mx = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) = #clean0rows(mx0, i) + countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c < #c mx0, #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≤ #clean0rows(mx, i), #clean0rows(mx0, i) ≤ #r mx0, #r mx0 ≤ # mx0[c]c, ∀ c1. c1 < #c mx0 → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i), ∀ c0. c0 < #c mx0 → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i) ⊦

Rule argument

Additional information

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

Proof step 68 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma count-add-even-odd-ind

Proof step 69 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  #c mx = #c mx0, #r mx = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) = #clean0rows(mx0, i) + countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx0, #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), c < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≤ #clean0rows(mx, i), ∀ c0. c0 < #c mx0 → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ c1. c1 < #c mx0 → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

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

Proof step 70 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 71:

  c0 < #c mx0 ⊦ countevn(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2

• Proof step 72:

  #c mx = #c mx0, #r mx = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) = #clean0rows(mx0, i) + countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c < #c mx0, #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≤ #clean0rows(mx, i), #clean0rows(mx0, i) ≤ #r mx0, countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2, ∀ c1. c1 < #c mx0 → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i), ∀ c0. c0 < #c mx0 → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i) ⊦

Rule argument

Additional information

Used terms: c, mx0, i

Proof step 71 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma countevn-maxcol0-bounded

Proof step 72 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 73:

  c0 < #c mx0 ⊦ countodd(mx0[c0]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2

• Proof step 74:

  #c mx = #c mx0, #r mx = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) = #clean0rows(mx0, i) + countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx0, #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), c < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2, #clean0rows(mx0, i) ≤ #r mx0, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≤ #clean0rows(mx, i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2, ∀ c0. c0 < #c mx0 → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ c1. c1 < #c mx0 → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

Used terms: c, mx0, i

Proof step 73 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Lemma countodd-maxcol0-bounded

Proof step 74 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 75:

  #c mx = #c mx0, #r mx = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) = #clean0rows(mx0, i) + countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c < #c mx0, #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < #dirtyrows(mx, i), countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < #dirtyrows(mx, i), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2, #clean0rows(mx0, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) ≤ #clean0rows(mx, i), #clean0rows(mx0, i) ≤ #r mx0, countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2, ∀ c1. c1 < #c mx0 → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i), ∀ c0. c0 < #c mx0 → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i) ⊦

Rule argument

Additional information

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

Proof step 75 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 76:

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

• Proof step 77:

  #c mx = #c mx0, #r mx = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) = #clean0rows(mx0, i) + countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx0, countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < #dirtyrows(mx, i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < #dirtyrows(mx, i), #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), c < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2, #clean0rows(mx0, i) ≤ #r mx0, countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2, ∀ c0. c0 < #c mx0 → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i), ∀ c1. c1 < #c mx0 → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i), ∃ n0. ( #clean0rows(mx0, i) + min (countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i))) + n0 = #clean0rows(mx, i) ⊦

Rule argument

Additional information

Used terms: #clean0rows(mx0, i) + min (countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)), #clean0rows(mx, i)

Proof step 76 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

A spec-lemma

Proof step 77 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 78:

  #c mx = #c mx0, #r mx = #r mx0, ( #clean0rows(mx0, i) + min (countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i))) + n0 = #clean0rows(mx, i), #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) = #clean0rows(mx0, i) + countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), c < #c mx0, #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < #dirtyrows(mx, i), countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < #dirtyrows(mx, i), scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2, #clean0rows(mx0, i) ≤ #r mx0, countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2, ∀ c1. c1 < #c mx0 → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i), ∀ c0. c0 < #c mx0 → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + #clean0rows(mx, i) ⊦

Rule argument

Additional information

Proof step 78 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 79:

  #c mx = #c mx0, #r mx = #r mx0, #dirtyrows(mx, i) + ( #clean0rows(mx0, i) + min (countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i))) + n0 = #clean0rows(mx0, i) + countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx, i) + ( ( #clean0rows(mx0, i) + min (countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i))) + n0) + #clean1rows(mx, i) = #r mx0, countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < #dirtyrows(mx, i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < #dirtyrows(mx, i), #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), c < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2, #clean0rows(mx0, i) ≤ #r mx0, countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2, ∀ c0. c0 < #c mx0 → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + ( #clean0rows(mx0, i) + min (countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i))) + n0, ∀ c1. c1 < #c mx0 → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

Proof step 79 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  #c mx = #c mx0, #r mx = #r mx0, #dirtyrows(mx0, i) + #clean1rows(mx0, i) = #clean1rows(mx, i) + countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #dirtyrows(mx, i) + min(countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)) + n0 = countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) + countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx, i) + ( ( #clean0rows(mx0, i) + min (countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i))) + n0) + #clean1rows(mx, i) = #r mx0, countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < #dirtyrows(mx, i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) < #dirtyrows(mx, i), #dirtyrows(mx0, i) /↑ 2 < #dirtyrows(mx, i), c < #c mx0, scolsorted(mx, #c mx0, mx0), srowsorted(mx0, #r mx0, mx0), countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2, #clean0rows(mx0, i) ≤ #r mx0, countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i) ≤ #dirtyrows(mx0, i) /↑ 2, ∀ c0. c0 < #c mx0 → count(mx[c0]c, λ j. j < i) ≤ #dirtyrows(mx, i) + ( #clean0rows(mx0, i) + min (countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i))) + n0, ∀ c1. c1 < #c mx0 → count(mx[c1]c, λ j. j < i) ≤ count(mx[c]c, λ j. j < i) ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 80 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 81:

  ⊦ m < n → min(m, n) = m

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = m + n0 ↔ n = n0; (s) eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (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 fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ m +1 = m + 1; (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 < n → min(m, n) = n; (s) min-a: ⊦ min(m, min(n, n0)) = min(min(m, n), n0); from specification nat-even min-c: ⊦ min(m, n) = min(n, m); from specification nat-even ⊦ m < n ↔ ¬ n ≤ m; (ss) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat Used terms: countevn(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i), countodd(mx0[c]c, #clean0rows(mx0, i), #r mx0, λ j. j < i)

Proof step 81 from proof scolsort-dirtyboundhalf (previous step) (back to tree)

A spec-lemma