Proof step 1 from proof allperm-permtoArr-ind (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, r ≤ #r mx0, ¬ perm(toArr(mx0, r), toArr(mx, r)), ∀ r0. r0 < r → perm(mx0[r0]r, mx[r0]r) ⊦

Rule argument

Additional information

Proof step 2 from proof allperm-permtoArr-ind (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  #c mx = #c mx0, #r mx = #r mx0, r0 +1 ≤ #r mx0, ¬ perm(toArr(mx0, r0 +1), toArr(mx, r0 +1)), ∀ r1. r1 < r0 +1 → perm(mx0[r1]r, mx[r1]r), ∀ mx, mx0. ¬ ( #c mx = #c mx0 ∧ #r mx = #r mx0 ∧ r0 ≤ #r mx0 ∧ ¬ perm(toArr(mx0, r0), toArr(mx, r0)) ∧ (∀ r1. r1 < r0 → perm(mx0[r1]r, mx[r1]r))) ⊦

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;; ⊦ 0 ≤ m; (s) ⊦ toArr(mx, 0) = []; (s) ⊦ perm([], []); (s)

Proof step 3 from proof allperm-permtoArr-ind (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  #c mx = #c mx0, #r mx = #r mx0, r0 < #r mx0, ¬ perm(toArr(mx0, r0) + mx0[r0]r, toArr(mx, r0) + mx[r0]r), ∀ r1. ¬ r0 < r1 → perm(mx0[r1]r, mx[r1]r), ∀ mx1, mx2. #c mx1 ≠ #c mx2 ∨ #r mx1 ≠ #r mx2 ∨ ¬ r0 ≤ #r mx2 ∨ perm(toArr(mx2, r0), toArr(mx1, r0)) ∨ ¬(∀ r1. r1 < r0 → perm(mx2[r1]r, mx1[r1]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 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) ⊦ m +1 = m + 1; (s) ⊦ toArr(mx, m + 1) = toArr(mx, m) + mx[m]r; (s) ⊦ m + 1 ≤ n ↔ m < n; (s)

Proof step 4 from proof allperm-permtoArr-ind (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 5:

  #c mx = #c mx0, #r mx = #r mx0, r0 < #r mx0, ¬ perm(toArr(mx0, r0) + mx0[r0]r, toArr(mx, r0) + mx[r0]r), ∀ r1. ¬ r0 < r1 → perm(mx0[r1]r, mx[r1]r), #c mx ≠ #c mx0 ∨ #r mx ≠ #r mx0 ∨ ¬ r0 ≤ #r mx0 ∨ perm(toArr(mx0, r0), toArr(mx, r0)) ∨ ¬(∀ r1. r1 < r0 → perm(mx0[r1]r, mx[r1]r)) ⊦

Rule argument

Additional information

Used terms: mx, mx0

Proof step 5 from proof allperm-permtoArr-ind (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, r0 < #r mx0, ¬ perm(toArr(mx0, r0) + mx0[r0]r, toArr(mx, r0) + mx[r0]r), ∀ r1. ¬ r0 < r1 → perm(mx0[r1]r, mx[r1]r), perm(toArr(mx0, r0), toArr(mx, r0)) ∨ ¬(r1 < r0 → perm(mx0[r1]r, mx[r1]r)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s)

Proof step 6 from proof allperm-permtoArr-ind (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  #c mx = #c mx0, #r mx = #r mx0, r0 < #r mx0, perm(toArr(mx0, r0), toArr(mx, r0)), ¬ perm(toArr(mx0, r0) + mx0[r0]r, toArr(mx, r0) + mx[r0]r), ∀ r1. ¬ r0 < r1 → perm(mx0[r1]r, mx[r1]r) ⊦

• Proof step 11:

  #c mx = #c mx0, #r mx = #r mx0, r1 < r0, r0 < #r mx0, ¬ perm(mx0[r1]r, mx[r1]r), ¬ perm(toArr(mx0, r0) + mx0[r0]r, toArr(mx, r0) + mx[r0]r), ∀ r1. ¬ r0 < r1 → perm(mx0[r1]r, mx[r1]r) ⊦

Rule argument

Additional information

Proof step 7 from proof allperm-permtoArr-ind (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  perm(x, x0), perm(y, y0) ⊦ perm(x + y, x0 + y0)

• Proof step 9:

  #c mx = #c mx0, #r mx = #r mx0, r0 < #r mx0, perm(toArr(mx0, r0), toArr(mx, r0)), ¬ perm(toArr(mx0, r0) + mx0[r0]r, toArr(mx, r0) + mx[r0]r), ∀ r1. ¬ r0 < r1 → perm(mx0[r1]r, mx[r1]r) ⊦ perm(toArr(mx0, r0), toArr(mx, r0)) ∧ perm(mx0[r0]r, mx[r0]r)

Rule argument

Additional information

Used terms: toArr(mx0, r0), mx0[r0]r, toArr(mx, r0), mx[r0]r

Proof step 8 from proof allperm-permtoArr-ind (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof allperm-permtoArr-ind (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, r0 < #r mx0, perm(toArr(mx0, r0), toArr(mx, r0)), ¬ perm(toArr(mx0, r0) + mx0[r0]r, toArr(mx, r0) + mx[r0]r), ¬ perm(mx0[r0]r, mx[r0]r), ∀ r1. ¬ r0 < r1 → perm(mx0[r1]r, mx[r1]r) ⊦

Rule argument

Additional information

Proof step 10 from proof allperm-permtoArr-ind (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < n; (s) Used terms: r0

Proof step 11 from proof allperm-permtoArr-ind (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, r1 + 1 < #r mx0, r0 < #r mx0, r1 < r0, r1 < #r mx0, ¬ perm(mx0[r1]r, mx[r1]r), ¬ perm(toArr(mx0, r0) + mx0[r0]r, toArr(mx, r0) + mx[r0]r), ∀ r1. ¬ r0 < r1 → perm(mx0[r1]r, mx[r1]r) ⊦

Rule argument

Additional information

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

Proof step 12 from proof allperm-permtoArr-ind (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; (s) Used terms: r1