Proof step 1 from proof dirytrows-leone (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  #c mx ≠ 0, #dirtyrows(mx, i) ≤ 1 ⊦ ∀ r. r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0, ∃ r0. count(mx[r0]r, λ j. j < i) ≠ 0 ∧ count(mx[r0]r, λ j. ¬ j < i) ≠ 0 ∧ (∀ r. r ≠ r0 ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

Proof step 2 from proof dirytrows-leone (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  #c mx ≠ 0, count(mx[r]r, λ j. ¬ j < i) ≠ 0, count(mx[r]r, λ j. j < i) ≠ 0, r < #r mx, #dirtyrows(mx, i) ≤ 1 ⊦ ∃ r0. count(mx[r0]r, λ j. j < i) ≠ 0 ∧ count(mx[r0]r, λ j. ¬ j < i) ≠ 0 ∧ (∀ r. r ≠ r0 ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0)

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 dirytrows-leone (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, count(mx[r]r, λ j. ¬ j < i) ≠ 0, count(mx[r]r, λ j. j < i) ≠ 0, r < #r mx, #dirtyrows(mx, i) ≤ 1 ⊦ ∃ r0. count(mx[r0]r, λ j. j < i) ≠ 0 ∧ count(mx[r0]r, λ j. ¬ j < i) ≠ 0 ∧ (∀ r. r ≠ r0 ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

Used terms: mx, i

Proof step 4 from proof dirytrows-leone (previous step) (back to tree)

Lemma dirtyrows-def

Proof step 5 from proof dirytrows-leone (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ m ≠ 0 → (m ≤ 1 ↔ m = 1)

• Proof step 7:

  #dirtyrows(mx, i) = 0, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, count(mx[r]r, λ j. ¬ j < i) ≠ 0, count(mx[r]r, λ j. j < i) ≠ 0, r < #r mx, #dirtyrows(mx, i) ≤ 1 ⊦ ∃ r0. count(mx[r0]r, λ j. j < i) ≠ 0 ∧ count(mx[r0]r, λ j. ¬ j < i) ≠ 0 ∧ (∀ r. r ≠ r0 ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0)

• Proof step 13:

  #dirtyrows(mx, i) = 1, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, #dirtyrows(mx, i) ≠ 0, count(mx[r]r, λ j. ¬ j < i) ≠ 0, count(mx[r]r, λ j. j < i) ≠ 0, r < #r mx ⊦ ∃ r0. count(mx[r0]r, λ j. j < i) ≠ 0 ∧ count(mx[r0]r, λ j. ¬ j < i) ≠ 0 ∧ (∀ r. r ≠ r0 ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

Used terms: #dirtyrows(mx, i)

Proof step 6 from proof dirytrows-leone (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof dirytrows-leone (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  #dirtyrows(mx, i) = 0, #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, count(mx[r]r, λ j. ¬ j < i) ≠ 0, count(mx[r]r, λ j. j < i) ≠ 0, r < #r mx ⊦ ∃ r0. count(mx[r0]r, λ j. j < i) ≠ 0 ∧ count(mx[r0]r, λ j. ¬ j < i) ≠ 0 ∧ (∀ r. r ≠ r0 ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

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

Proof step 8 from proof dirytrows-leone (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  #dirtyrows(mx, i) = 0, #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, count(mx[r]r, λ j. ¬ j < i) ≠ 0, count(mx[r]r, λ j. j < i) ≠ 0, r < #r mx, r < #clean0rows(mx, i) → count(mx[r]r, λ j. ¬ j < i) = 0 ⊦ ∃ r0. count(mx[r0]r, λ j. j < i) ≠ 0 ∧ count(mx[r0]r, λ j. ¬ j < i) ≠ 0 ∧ (∀ r. r ≠ r0 ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

Used terms: r, mx, i

Proof step 9 from proof dirytrows-leone (previous step) (back to tree)

Lemma clean0rows-allls

Proof step 10 from proof dirytrows-leone (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  #dirtyrows(mx, i) = 0, #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, #clean1rows(mx, i) ≠ 0, count(mx[r]r, λ j. ¬ j < i) ≠ 0, count(mx[r]r, λ j. j < i) ≠ 0, r < #r mx, #clean0rows(mx, i) < #r mx, #clean0rows(mx, i) ≤ r ⊦ ∃ r0. count(mx[r0]r, λ j. j < i) ≠ 0 ∧ count(mx[r0]r, λ j. ¬ j < i) ≠ 0 ∧ (∀ r. r ≠ r0 ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

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

Proof step 11 from proof dirytrows-leone (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m ≤ n → (n < m ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: mx, i, r

Proof step 12 from proof dirytrows-leone (previous step) (back to tree)

Lemma clean1rows-allge

Proof step 13 from proof dirytrows-leone (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  #dirtyrows(mx, i) = 1, 1 + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, count(mx[r]r, λ j. j < i) ≠ 0, count(mx[r]r, λ j. ¬ j < i) ≠ 0, r < #r mx, r ≤ #clean0rows(mx, i) + #clean1rows(mx, i) ⊦ ∃ r0. count(mx[r0]r, λ j. j < i) ≠ 0 ∧ count(mx[r0]r, λ j. ¬ j < i) ≠ 0 ∧ (∀ r. r ≠ r0 ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

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

Proof step 14 from proof dirytrows-leone (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 15:

  #dirtyrows(mx, i) = 1, 1 + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, r < #r mx, r ≤ #clean0rows(mx, i) + #clean1rows(mx, i) ⊦ ∃ r0. count(mx[r0]r, λ j. j < i) ≠ 0 ∧ count(mx[r0]r, λ j. ¬ j < i) ≠ 0 ∧ (∀ r. r ≠ r0 ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

Proof step 15 from proof dirytrows-leone (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 16:

  #dirtyrows(mx, i) = 1, 1 + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, r < #r mx, r ≤ #clean0rows(mx, i) + #clean1rows(mx, i) ⊦ count(mx[#clean0rows(mx, i)]r, λ j. j < i) ≠ 0 ∧ count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0 ∧ (∀ r. r ≠ #clean0rows(mx, i) ∧ r < #r mx → count(mx[r]r, λ j. j < i) = 0 ∨ count(mx[r]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

Used terms: #clean0rows(mx, i)

Proof step 16 from proof dirytrows-leone (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  #dirtyrows(mx, i) = 1, 1 + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, r < #r mx, r ≤ #clean0rows(mx, i) + #clean1rows(mx, i) ⊦ count(mx[#clean0rows(mx, i)]r, λ j. j < i) ≠ 0 ∧ count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0 ∧ (r0 ≠ #clean0rows(mx, i) ∧ r0 < #r mx → count(mx[r0]r, λ j. j < i) = 0 ∨ count(mx[r0]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

Proof step 17 from proof dirytrows-leone (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  #dirtyrows(mx, i) = 1, 1 + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, r < #r mx, r ≤ #clean0rows(mx, i) + #clean1rows(mx, i), #clean0rows(mx, i) < #r mx → count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0 ⊦ count(mx[#clean0rows(mx, i)]r, λ j. j < i) ≠ 0 ∧ count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0 ∧ (r0 ≠ #clean0rows(mx, i) ∧ r0 < #r mx → count(mx[r0]r, λ j. j < i) = 0 ∨ count(mx[r0]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

Used terms: mx, i

Proof step 18 from proof dirytrows-leone (previous step) (back to tree)

Lemma clean0rows-notallls

Proof step 19 from proof dirytrows-leone (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 20:

  #c mx ≠ 0 ⊦ ¬ #r mx < #clean0rows(mx, i) + #clean1rows(mx, i)

• Proof step 21:

  #dirtyrows(mx, i) = 1, 1 + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, r < #r mx, r ≤ #clean0rows(mx, i) + #clean1rows(mx, i), ¬ #r mx < #clean0rows(mx, i) + #clean1rows(mx, i), #clean0rows(mx, i) < #r mx → count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0 ⊦ count(mx[#clean0rows(mx, i)]r, λ j. j < i) ≠ 0 ∧ count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0 ∧ (r0 ≠ #clean0rows(mx, i) ∧ r0 < #r mx → count(mx[r0]r, λ j. j < i) = 0 ∨ count(mx[r0]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

Used terms: mx, i

Proof step 20 from proof dirytrows-leone (previous step) (back to tree)

Lemma clean0-plus-clean1-bounded

Proof step 21 from proof dirytrows-leone (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  #dirtyrows(mx, i) = 1, 1 + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, r < #r mx, #clean0rows(mx, i) + #clean1rows(mx, i) ≤ #r mx, r ≤ #clean0rows(mx, i) + #clean1rows(mx, i), #clean0rows(mx, i) < #r mx → count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0 ⊦ count(mx[#clean0rows(mx, i)]r, λ j. j < i) ≠ 0 ∧ count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0 ∧ (r0 ≠ #clean0rows(mx, i) ∧ r0 < #r mx → count(mx[r0]r, λ j. j < i) = 0 ∨ count(mx[r0]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 22 from proof dirytrows-leone (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 23:

  #dirtyrows(mx, i) = 1, 1 + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0, r < #r mx, r ≤ #clean0rows(mx, i) + #clean1rows(mx, i), #clean0rows(mx, i) + #clean1rows(mx, i) ≤ #r mx ⊦ count(mx[#clean0rows(mx, i)]r, λ j. j < i) ≠ 0 ∧ count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0 ∧ (r0 ≠ #clean0rows(mx, i) ∧ r0 < #r mx → count(mx[r0]r, λ j. j < i) = 0 ∨ count(mx[r0]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

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

Proof step 23 from proof dirytrows-leone (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  #dirtyrows(mx, i) = 1, 1 + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0, r < #r mx, #clean0rows(mx, i) + #clean1rows(mx, i) ≤ #r mx, r ≤ #clean0rows(mx, i) + #clean1rows(mx, i) ⊦ count(mx[#clean0rows(mx, i)]r, λ j. j < i) ≠ 0 ∧ (r0 ≠ #clean0rows(mx, i) ∧ r0 < #r mx → count(mx[r0]r, λ j. j < i) = 0 ∨ count(mx[r0]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

Proof step 24 from proof dirytrows-leone (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

  #dirtyrows(mx, i) = 1, 1 + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0, r < #r mx, r ≤ #clean0rows(mx, i) + #clean1rows(mx, i), #clean0rows(mx, i) + #clean1rows(mx, i) ≤ #r mx, #clean1rows(mx, i) + #clean0rows(mx, i) + 1 = #r mx → count(mx[#clean0rows(mx, i)]r, λ j. j < i) ≠ 0 ⊦ count(mx[#clean0rows(mx, i)]r, λ j. j < i) ≠ 0 ∧ (r0 ≠ #clean0rows(mx, i) ∧ r0 < #r mx → count(mx[r0]r, λ j. j < i) = 0 ∨ count(mx[r0]r, λ j. ¬ j < i) = 0)

Rule argument

Additional information

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

Proof step 25 from proof dirytrows-leone (previous step) (back to tree)

Lemma clean1rows-notallge

Proof step 26 from proof dirytrows-leone (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  #dirtyrows(mx, i) = 1, 1 + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0, count(mx[#clean0rows(mx, i)]r, λ j. j < i) ≠ 0, count(mx[r0]r, λ j. j < i) ≠ 0, count(mx[r0]r, λ j. ¬ j < i) ≠ 0, r0 ≠ #clean0rows(mx, i), r < #r mx, r0 < #r mx, r0 ≤ #clean0rows(mx, i) + #clean1rows(mx, i), #clean0rows(mx, i) + #clean1rows(mx, i) ≤ #r mx, r ≤ #clean0rows(mx, i) + #clean1rows(mx, i) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ 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) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic

Proof step 27 from proof dirytrows-leone (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 28:

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

• Proof step 29:

  #dirtyrows(mx, i) = 1, 1 + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0, count(mx[#clean0rows(mx, i)]r, λ j. j < i) ≠ 0, count(mx[r0]r, λ j. j < i) ≠ 0, count(mx[r0]r, λ j. ¬ j < i) ≠ 0, r0 ≠ #clean0rows(mx, i), r0 < #r mx, r < #r mx, r ≤ #clean0rows(mx, i) + #clean1rows(mx, i), #clean0rows(mx, i) + #clean1rows(mx, i) ≤ #r mx, r0 ≤ #clean0rows(mx, i) + #clean1rows(mx, i), r0 < #clean0rows(mx, i) → count(mx[r0]r, λ j. ¬ j < i) = 0 ⊦

Rule argument

Additional information

Used terms: r0, mx, i

Proof step 28 from proof dirytrows-leone (previous step) (back to tree)

Lemma clean0rows-allls

Proof step 29 from proof dirytrows-leone (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  #dirtyrows(mx, i) = 1, 1 + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx, #c mx ≠ 0, #clean1rows(mx, i) ≠ 0, count(mx[#clean0rows(mx, i)]r, λ j. ¬ j < i) ≠ 0, count(mx[#clean0rows(mx, i)]r, λ j. j < i) ≠ 0, count(mx[r0]r, λ j. j < i) ≠ 0, count(mx[r0]r, λ j. ¬ j < i) ≠ 0, r0 ≠ #clean0rows(mx, i), r < #r mx, r0 < #r mx, #clean0rows(mx, i) < r0, #clean0rows(mx, i) < #r mx, r0 ≤ #clean0rows(mx, i) + #clean1rows(mx, i), #clean0rows(mx, i) + #clean1rows(mx, i) ≤ #r mx, r ≤ #clean0rows(mx, i) + #clean1rows(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 ⊦ ¬ m + n < m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m < m + n ↔ n ≠ 0; (s) ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≠ n → (m < n ↔ ¬ n < m); (ss)

Proof step 30 from proof dirytrows-leone (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 31:

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

Rule argument

Additional information

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

Proof step 31 from proof dirytrows-leone (previous step) (back to tree)

Lemma clean1rows-allge