Proof step 1 from proof rowperms-dirtyrowsunchanged (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, ¬(#dirtyrows(mx0, i) = #dirtyrows(mx, i) ↔ true), ∀ r. r < #r mx → perm(mx0[r]r, mx[r]r) ⊦

Rule argument

Additional information

Proof step 2 from proof rowperms-dirtyrowsunchanged (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, #dirtyrows(mx0, i) ≠ #dirtyrows(mx, i), ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦

Rule argument

Additional information

Proof step 3 from proof rowperms-dirtyrowsunchanged (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:

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

Rule argument

Additional information

Used terms: i, mx

Proof step 4 from proof rowperms-dirtyrowsunchanged (previous step) (back to tree)

Lemma dirtyrows-def

Proof step 5 from proof rowperms-dirtyrowsunchanged (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, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx0, #c mx0 ≠ 0, #dirtyrows(mx0, i) ≠ #dirtyrows(mx, i), ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦

Rule argument

Additional information

Proof step 6 from proof rowperms-dirtyrowsunchanged (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  #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, #c mx0 ≠ 0, #dirtyrows(mx0, i) ≠ #dirtyrows(mx, i), ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦

Rule argument

Additional information

Used terms: i, mx0

Proof step 7 from proof rowperms-dirtyrowsunchanged (previous step) (back to tree)

Lemma dirtyrows-def

Proof step 8 from proof rowperms-dirtyrowsunchanged (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  #c mx = #c mx0, #r mx = #r mx0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx0, #c mx0 ≠ 0, #dirtyrows(mx0, i) ≠ #dirtyrows(mx, i), ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦ #c mx ≠ 0 ∧ (∀ r. r < #r mx → perm(mx0[r]r, mx[r]r))

• Proof step 12:

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

Rule argument

Additional information

Used terms: mx, mx0, i

Proof step 9 from proof rowperms-dirtyrowsunchanged (previous step) (back to tree)

Lemma rowperms-clean0unchanged

Proof step 10 from proof rowperms-dirtyrowsunchanged (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  #c mx = #c mx0, #r mx = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx0, #dirtyrows(mx0, i) + #clean0rows(mx0, i) + #clean1rows(mx0, i) = #r mx0, #c mx0 ≠ 0, #dirtyrows(mx0, i) ≠ #dirtyrows(mx, i), r < #r mx0, ¬ perm(mx0[r]r, mx[r]r), ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦

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 11 from proof rowperms-dirtyrowsunchanged (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 12 from proof rowperms-dirtyrowsunchanged (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

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

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 13 from proof rowperms-dirtyrowsunchanged (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  #c mx = #c mx0, #clean0rows(mx0, i) = #clean0rows(mx, i), #r mx = #r mx0, #dirtyrows(mx0, i) + #clean1rows(mx0, i) = #clean1rows(mx, i) + #dirtyrows(mx, i), #dirtyrows(mx0, i) + #clean0rows(mx, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx0, #c mx0 ≠ 0, #dirtyrows(mx0, i) ≠ #dirtyrows(mx, i), ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦ #c mx ≠ 0 ∧ (∀ r. r < #r mx → perm(mx0[r]r, mx[r]r))

Rule argument

Additional information

Used simplifier rules: eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (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 Used terms: mx, mx0, i

Proof step 14 from proof rowperms-dirtyrowsunchanged (previous step) (back to tree)

Lemma rowperms-clean1unchanged

Proof step 15 from proof rowperms-dirtyrowsunchanged (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  #c mx = #c mx0, #clean0rows(mx0, i) = #clean0rows(mx, i), #r mx = #r mx0, #dirtyrows(mx, i) + #clean0rows(mx, i) + #clean1rows(mx, i) = #r mx0, #dirtyrows(mx0, i) + #clean0rows(mx, i) + #clean1rows(mx0, i) = #r mx0, #dirtyrows(mx0, i) + #clean1rows(mx0, i) = #clean1rows(mx, i) + #dirtyrows(mx, i), #c mx0 ≠ 0, #dirtyrows(mx0, i) ≠ #dirtyrows(mx, i), r < #r mx0, ¬ perm(mx0[r]r, mx[r]r), ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦

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 16 from proof rowperms-dirtyrowsunchanged (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r