Proof step 1 from proof srowsorted-dirtyboundunchanged (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, mx0.dirtyrows≤(bound), srowsorted(mx, #r mx0, mx0), ¬ mx.dirtyrows≤(bound) ⊦

Rule argument

Additional information

Proof step 2 from proof srowsorted-dirtyboundunchanged (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 mx = #c mx0, #r mx = #r mx0, #c mx ≠ 0, srowsorted(mx, #r mx0, mx0), ¬ mx.dirtyrows≤(bound), ∀ i. #dirtyrows(mx0, i) ≤ bound ⊦

Rule argument

Additional information

Used terms: mx0, bound

Proof step 3 from proof srowsorted-dirtyboundunchanged (previous step) (back to tree)

Lemma dirtyrowsbound-def

Proof step 4 from proof srowsorted-dirtyboundunchanged (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

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

Rule argument

Additional information

Used terms: mx, bound

Proof step 5 from proof srowsorted-dirtyboundunchanged (previous step) (back to tree)

Lemma dirtyrowsbound-def

Proof step 6 from proof srowsorted-dirtyboundunchanged (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  #c mx = #c mx0, #r mx = #r mx0, #c mx0 ≠ 0, bound < #dirtyrows(mx, i), srowsorted(mx, #r mx0, 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 7 from proof srowsorted-dirtyboundunchanged (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

Used terms: i

Proof step 8 from proof srowsorted-dirtyboundunchanged (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, bound < #dirtyrows(mx, i), #dirtyrows(mx0, i) < #dirtyrows(mx, i), srowsorted(mx, #r mx0, mx0), #dirtyrows(mx0, i) ≤ bound ⊦

Rule argument

Additional information

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

Proof step 9 from proof srowsorted-dirtyboundunchanged (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 10:

  #r mx = #r mx0, #c mx = #c mx0, #c mx ≠ 0, ∀ r. r < #r mx → perm(mx0[r]r, mx[r]r) ⊦ #dirtyrows(mx0, i) = #dirtyrows(mx, i) ↔ true

Rule argument

Additional information

Used simplifier rules: srowsorted-permrow: #r mx = #r mx0, r < #r mx ⊦ srowsorted(mx, #r mx0, mx0) → perm(mx0[r]r, mx[r]r); 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 trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n → ¬ n < m; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ m ≤ n → (n < m ↔ false); (s) Used terms: mx, mx0, i

Proof step 10 from proof srowsorted-dirtyboundunchanged (previous step) (back to tree)

Lemma rowperms-dirtyrowsunchanged