Proof step 1 from proof srowsorted-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, srowsorted(mx, r, mx0), m ≤ #r mx0, r ≤ #r mx0, ¬ perm(toArr(mx0, m), toArr(mx, m)) ⊦

Rule argument

Additional information

Proof step 2 from proof srowsorted-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, srowsorted(mx, r, mx0), r ≤ #r mx0, m0 +1 ≤ #r mx0, ¬ perm(toArr(mx0, m0 +1), toArr(mx, m0 +1)), ∀ mx, mx0, r. ¬ (#c mx = #c mx0 ∧ #r mx = #r mx0 ∧ srowsorted(mx, r, mx0) ∧ m0 ≤ #r mx0 ∧ r ≤ #r mx0 ∧ ¬ perm(toArr(mx0, m0), toArr(mx, m0))) ⊦

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 srowsorted-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, m0 < #r mx0, srowsorted(mx, r, mx0), r ≤ #r mx0, ¬ perm(toArr(mx0, m0) + mx0[m0]r, toArr(mx, m0) + mx[m0]r), ∀ mx1, mx2, r0. #c mx1 ≠ #c mx2 ∨ #r mx1 ≠ #r mx2 ∨ ¬ srowsorted(mx1, r0, mx2) ∨ ¬ m0 ≤ #r mx2 ∨ ¬ r0 ≤ #r mx2 ∨ perm(toArr(mx2, m0), toArr(mx1, m0)) ⊦

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 ⊦ toArr(mx, m + 1) = toArr(mx, m) + mx[m]r; (s) ⊦ m +1 = m + 1; (s) ⊦ m + 1 ≤ n ↔ m < n; (s)

Proof step 4 from proof srowsorted-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, m0 < #r mx0, srowsorted(mx, r, mx0), r ≤ #r mx0, ¬ perm(toArr(mx0, m0) + mx0[m0]r, toArr(mx, m0) + mx[m0]r), #c mx ≠ #c mx0 ∨ #r mx ≠ #r mx0 ∨ ¬ srowsorted(mx, r, mx0) ∨ ¬ m0 ≤ #r mx0 ∨ ¬ r ≤ #r mx0 ∨ perm(toArr(mx0, m0), toArr(mx, m0)) ⊦

Rule argument

Additional information

Used terms: mx, mx0, r

Proof step 5 from proof srowsorted-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, m0 < #r mx0, perm(toArr(mx0, m0), toArr(mx, m0)), srowsorted(mx, r, mx0), r ≤ #r mx0, ¬ perm(toArr(mx0, m0) + mx0[m0]r, toArr(mx, m0) + mx[m0]r) ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ m ≤ #r mx → ( srowsorted(mx, m, mx0) ↔ #r mx = #r mx0 ∧ #c mx = #c mx0 ∧ (∀ r. r < #r mx → (r < m ⊃ perm(mx0[r]r, mx[r]r) ∧ ordered≤((even(r) ⊃ mx[r]r;rev(mx[r]r)));mx0[r]r = mx[r]r)))

• Proof step 8:

  #c mx = #c mx0, #r mx = #r mx0, m0 < #r mx0, perm(toArr(mx0, m0), toArr(mx, m0)), r ≤ #r mx0, r ≤ #r mx, ¬ perm(toArr(mx0, m0) + mx0[m0]r, toArr(mx, m0) + mx[m0]r), ∀ r0. r0 < #r mx → (r0 < r ⊃ perm(mx0[r0]r, mx[r0]r) ∧ ordered≤((even(r0) ⊃ mx[r0]r;rev(mx[r0]r)));mx0[r0]r = mx[r0]r) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (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 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 ≠ 0; (s) ⊦ ¬ n < n; (s) Used terms: mx, r, mx0

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

Lemma srowsorted-def

Proof step 8 from proof srowsorted-permtoArr-ind (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, m0 < #r mx0, perm(toArr(mx0, m0), toArr(mx, m0)), r ≤ #r mx0, ¬ perm(toArr(mx0, m0) + mx0[m0]r, toArr(mx, m0) + mx[m0]r), ∀ r0. r0 < #r mx0 → (r0 < r ⊃ perm(mx0[r0]r, mx[r0]r) ∧ ordered≤((even(r0) ⊃ mx[r0]r;rev(mx[r0]r)));mx0[r0]r = mx[r0]r) ⊦

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 10:

  #c mx = #c mx0, #r mx = #r mx0, m0 < #r mx0, perm(toArr(mx0, m0), toArr(mx, m0)), r ≤ #r mx0, ¬ perm(toArr(mx0, m0) + mx0[m0]r, toArr(mx, m0) + mx[m0]r), m0 < #r mx0 → (m0 < r ⊃ perm(mx0[m0]r, mx[m0]r) ∧ ordered≤((even(m0) ⊃ mx[m0]r;rev(mx[m0]r)));mx0[m0]r = mx[m0]r), ∀ r0. r0 < #r mx0 → (r0 < r ⊃ perm(mx0[r0]r, mx[r0]r) ∧ ordered≤((even(r0) ⊃ mx[r0]r;rev(mx[r0]r)));mx0[r0]r = mx[r0]r) ⊦

Rule argument

Additional information

Used terms: m0

Proof step 10 from proof srowsorted-permtoArr-ind (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, m0 < #r mx0, perm(toArr(mx0, m0), toArr(mx, m0)), r ≤ #r mx0, ¬ perm(toArr(mx0, m0) + mx0[m0]r, toArr(mx, m0) + mx[m0]r), (m0 < r ⊃ perm(mx0[m0]r, mx[m0]r) ∧ ordered≤((even(m0) ⊃ mx[m0]r;rev(mx[m0]r)));mx0[m0]r = mx[m0]r), ∀ r0. r0 < #r mx0 → (r0 < r ⊃ perm(mx0[r0]r, mx[r0]r) ∧ ordered≤((even(r0) ⊃ mx[r0]r;rev(mx[r0]r)));mx0[r0]r = mx[r0]r) ⊦

Rule argument

Additional information

Proof step 11 from proof srowsorted-permtoArr-ind (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 12:

  #c mx = #c mx0, #r mx = #r mx0, m0 < #r mx0, m0 < r, ordered≤((even(m0) ⊃ mx[m0]r;rev(mx[m0]r))), perm(toArr(mx0, m0), toArr(mx, m0)), perm(mx0[m0]r, mx[m0]r), r ≤ #r mx0, ¬ perm(toArr(mx0, m0) + mx0[m0]r, toArr(mx, m0) + mx[m0]r), ∀ r0. r0 < #r mx0 → (r0 < r ⊃ perm(mx0[r0]r, mx[r0]r) ∧ ordered≤((even(r0) ⊃ mx[r0]r;rev(mx[r0]r)));mx0[r0]r = mx[r0]r) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n → m ≤ n; (s) ⊦ perm(x + y, z + y) ↔ perm(x, z); (s) a: ⊦ (x + y) + z = x + y + z; from specification list[oarray-sort-new]

Proof step 12 from proof srowsorted-permtoArr-ind (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

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

Proof step 13 from proof srowsorted-permtoArr-ind (previous step) (back to tree)

A spec-lemma