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

Rule argument

Additional information

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

Rule argument

Additional information

Proof step 3 from proof rowperms-clean1unchanged (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

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

• Proof step 23:

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

Rule argument

Additional information

Used formulas: #clean1rows(mx0, i) < #clean1rows(mx, i)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

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

Rule argument

Additional information

Used terms: i, mx

Proof step 5 from proof rowperms-clean1unchanged (previous step) (back to tree)

Lemma clean1rows-bounded

Proof step 6 from proof rowperms-clean1unchanged (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, #clean1rows(mx0, i) ≠ #clean1rows(mx, i), #clean1rows(mx0, i) < #clean1rows(mx, i), #clean1rows(mx0, i) < #r mx0, #clean1rows(mx, i) ≤ #r mx0, ∀ 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 fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

  #c mx = #c mx0, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx0, i) ≠ #clean1rows(mx, i), #clean1rows(mx0, i) < #r mx0, #clean1rows(mx0, i) < #clean1rows(mx, i), #clean1rows(mx, i) ≤ #r mx0, #clean1rows(mx0, i) + (#r mx - #clean1rows(mx0, i) + 1) + 1 = #r mx0 → count(mx0[#r mx - #clean1rows(mx0, i) + 1]r, λ j. j < i) ≠ 0, ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦

Rule argument

Additional information

Used terms: mx0, i, #r mx - #clean1rows(mx0, i) + 1

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

Lemma clean1rows-notallge

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  #c mx = #c mx0, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx0, i) ≠ #clean1rows(mx, i), count(mx0[#r mx0 - #clean1rows(mx0, i) + 1]r, λ j. j < i) ≠ 0, #clean1rows(mx0, i) < #clean1rows(mx, i), #clean1rows(mx0, i) < #r mx0, #clean1rows(mx, i) ≤ #r mx0, ∀ 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 ⊦ m + n = m + n0 ↔ n = n0; (s) n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1; (s) ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m + 1 ≤ n ↔ m < n; (s)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  #c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx0, i) + 1, #c mx0 ≠ 0, #clean1rows(mx0, i) ≠ #clean1rows(mx, i), count(mx0[n0]r, λ j. j < i) ≠ 0, #clean1rows(mx0, i) < #r mx0, #clean1rows(mx0, i) < #clean1rows(mx, i), #clean1rows(mx, i) ≤ #r mx0, #clean1rows(mx0, i) + 1 ≤ #r mx0, ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ 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 n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: #r mx0, #clean1rows(mx0, i) + 1, n0

Proof step 11 from proof rowperms-clean1unchanged (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

  #c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx0, i) + 1, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx0, i) ≠ #clean1rows(mx, i), count(mx0[n0]r, λ j. j < i) ≠ 0, #clean1rows(mx0, i) < #clean1rows(mx, i), #clean1rows(mx0, i) < #r mx0, #clean1rows(mx, i) ≤ #r mx0, #r mx ≤ #clean1rows(mx, i) + n0 ∧ n0 < #r mx → count(mx[n0]r, λ j. j < i) = 0, ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦

Rule argument

Additional information

Used terms: mx, i, n0

Proof step 13 from proof rowperms-clean1unchanged (previous step) (back to tree)

Lemma clean1rows-allge

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  #c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx0, i) + 1, #c mx0 ≠ 0, #clean1rows(mx0, i) ≠ #clean1rows(mx, i), count(mx0[n0]r, λ j. j < i) ≠ 0, #clean1rows(mx0, i) < #r mx0, #clean1rows(mx0, i) < #clean1rows(mx, i), #clean1rows(mx, i) ≤ #r mx0, #r mx0 ≤ #clean1rows(mx, i) + n0 ∧ n0 < #r mx0 → count(mx[n0]r, λ j. j < i) = 0, ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 16:

  #c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx0, i) + 1, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx0, i) ≠ #clean1rows(mx, i), count(mx0[n0]r, λ j. j < i) ≠ 0, #clean1rows(mx0, i) < #clean1rows(mx, i), #clean1rows(mx0, i) < #r mx0, #clean1rows(mx, i) ≤ #r mx0, ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦ #r mx0 ≤ #clean1rows(mx, i) + n0 ∧ n0 < #r mx0

• Proof step 18:

  #c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx0, i) + 1, #r mx = #r mx0, count(mx[n0]r, λ j. j < i) = 0, #c mx0 ≠ 0, #clean1rows(mx0, i) ≠ #clean1rows(mx, i), count(mx0[n0]r, λ j. j < i) ≠ 0, #clean1rows(mx0, i) < #clean1rows(mx, i), #clean1rows(mx0, i) < #r mx0, #clean1rows(mx, i) ≤ #r mx0, ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦

Rule argument

Additional information

Proof step 16 from proof rowperms-clean1unchanged (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  #c mx = #c mx0, #r mx0 = n0 + #clean1rows(mx0, i) + 1, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx0, i) ≠ #clean1rows(mx, i), count(mx0[n0]r, λ j. j < i) ≠ 0, #clean1rows(mx0, i) < #clean1rows(mx, i), #clean1rows(mx0, i) < #r mx0, #clean1rows(mx0, i) < #clean1rows(mx, i) + n0, #clean1rows(mx0, i) < n0, #clean1rows(mx, i) ≤ #r mx0, #r mx0 ≤ #clean1rows(mx, i) + n0, #r mx0 ≤ n0, #clean1rows(mx, i) ≤ n0, ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦

Rule argument

Additional information

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

Proof step 17 from proof rowperms-clean1unchanged (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m + 1 ≤ n ↔ m < n; (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

Proof step 18 from proof rowperms-clean1unchanged (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ perm(x, y) → count(x, p) = count(y, p)

• Proof step 20:

  #c mx = #c mx0, #r mx = #r mx0, #r mx0 = n0 + #clean1rows(mx0, i) + 1, count(mx[n0]r, λ j. j < i) = 0, #c mx0 ≠ 0, #clean1rows(mx0, i) ≠ #clean1rows(mx, i), count(mx0[n0]r, λ j. j < i) ≠ 0, #clean1rows(mx0, i) < #r mx0, #clean1rows(mx0, i) < #clean1rows(mx, i), #clean1rows(mx, i) ≤ #r mx0, ¬ perm(mx0[n0]r, mx[n0]r), ∀ r. r < #r mx0 → perm(mx0[r]r, mx[r]r) ⊦

Rule argument

Additional information

Used terms: mx0[n0]r, mx[n0]r, λ j. j < i

Proof step 19 from proof rowperms-clean1unchanged (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof rowperms-clean1unchanged (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

Used terms: n0

Proof step 21 from proof rowperms-clean1unchanged (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

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

Rule argument

Additional information

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

Proof step 22 from proof rowperms-clean1unchanged (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (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

Proof step 23 from proof rowperms-clean1unchanged (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

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

Rule argument

Additional information

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

Proof step 24 from proof rowperms-clean1unchanged (previous step) (back to tree)

User applied rule apply proof lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

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

Rule argument

Additional information

Proof step 25 from proof rowperms-clean1unchanged (previous step) (back to tree)

Proof step 4 used as proof-lemma

Proof step 26 from proof rowperms-clean1unchanged (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  #c mx = #c mx0, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx0, i) ≠ #clean1rows(mx, i), r < #r mx0, #clean1rows(mx, i) < #clean1rows(mx0, i), ¬ perm(mx[r]r, mx0[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 27 from proof rowperms-clean1unchanged (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ perm(x, y) ↔ perm(y, x)

• Proof step 29:

  #c mx = #c mx0, #r mx = #r mx0, #c mx0 ≠ 0, #clean1rows(mx0, i) ≠ #clean1rows(mx, i), #clean1rows(mx, i) < #clean1rows(mx0, 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 terms: mx[r]r, mx0[r]r

Proof step 28 from proof rowperms-clean1unchanged (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof rowperms-clean1unchanged (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r