Proof step 1 from proof scolsorted-permtoArc-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, scolsorted(mx, c, mx0), m ≤ #c mx0, c ≤ #c mx0, ¬ perm(toArc(mx0, m), toArc(mx, m)) ⊦

Rule argument

Additional information

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

Rule argument

Additional information

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

Proof step 3 from proof scolsorted-permtoArc-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 < #c mx0, scolsorted(mx, c, mx0), c ≤ #c mx0, ¬ perm(toArc(mx0, m0) + mx0[m0]c, toArc(mx, m0) + mx[m0]c), ∀ mx1, mx2, c0. #c mx1 ≠ #c mx2 ∨ #r mx1 ≠ #r mx2 ∨ ¬ scolsorted(mx1, c0, mx2) ∨ ¬ m0 ≤ #c mx2 ∨ ¬ c0 ≤ #c mx2 ∨ perm(toArc(mx2, m0), toArc(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 ⊦ toArc(mx, m + 1) = toArc(mx, m) + mx[m]c; (s) ⊦ m +1 = m + 1; (s) ⊦ m + 1 ≤ n ↔ m < n; (s)

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

Rule argument

Additional information

Used terms: mx, mx0, c

Proof step 5 from proof scolsorted-permtoArc-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 < #c mx0, perm(toArc(mx0, m0), toArc(mx, m0)), scolsorted(mx, c, mx0), c ≤ #c mx0, ¬ perm(toArc(mx0, m0) + mx0[m0]c, toArc(mx, m0) + mx[m0]c) ⊦

Rule argument

Additional information

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

Proof step 6 from proof scolsorted-permtoArc-ind (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

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

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, c, mx0

Proof step 7 from proof scolsorted-permtoArc-ind (previous step) (back to tree)

Lemma scolsorted-def

Proof step 8 from proof scolsorted-permtoArc-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 < #c mx0, perm(toArc(mx0, m0), toArc(mx, m0)), c ≤ #c mx0, ¬ perm(toArc(mx0, m0) + mx0[m0]c, toArc(mx, m0) + mx[m0]c), ∀ c0. c0 < #c mx0 → (c0 < c ⊃ perm(mx0[c0]c, mx[c0]c) ∧ ordered≤(mx[c0]c);mx0[c0]c = mx[c0]c) ⊦

Rule argument

Additional information

Proof step 9 from proof scolsorted-permtoArc-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 < #c mx0, perm(toArc(mx0, m0), toArc(mx, m0)), c ≤ #c mx0, ¬ perm(toArc(mx0, m0) + mx0[m0]c, toArc(mx, m0) + mx[m0]c), m0 < #c mx0 → (m0 < c ⊃ perm(mx0[m0]c, mx[m0]c) ∧ ordered≤(mx[m0]c);mx0[m0]c = mx[m0]c) ⊦

Rule argument

Additional information

Used terms: m0

Proof step 10 from proof scolsorted-permtoArc-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 < #c mx0, perm(toArc(mx0, m0), toArc(mx, m0)), c ≤ #c mx0, ¬ perm(toArc(mx0, m0) + mx0[m0]c, toArc(mx, m0) + mx[m0]c), (m0 < c ⊃ perm(mx0[m0]c, mx[m0]c) ∧ ordered≤(mx[m0]c);mx0[m0]c = mx[m0]c) ⊦

Rule argument

Additional information

Proof step 11 from proof scolsorted-permtoArc-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 < #c mx0, m0 < c, ordered≤(mx[m0]c), perm(toArc(mx0, m0), toArc(mx, m0)), perm(mx0[m0]c, mx[m0]c), c ≤ #c mx0, ¬ perm(toArc(mx0, m0) + mx0[m0]c, toArc(mx, m0) + mx[m0]c) ⊦

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 scolsorted-permtoArc-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: toArc(mx0, m0), mx0[m0]c, toArc(mx, m0), mx[m0]c

Proof step 13 from proof scolsorted-permtoArc-ind (previous step) (back to tree)

A spec-lemma