Proof step 1 from proof descending-order-is-max-permuted (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ordered≤(rev(ar)), ¬ max(ar) ⊦

Rule argument

Additional information

Proof step 2 from proof descending-order-is-max-permuted (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ordered≤(rev([])), ¬ max([]) ⊦

• Proof step 9:

  ordered≤(rev(i + ar0)), ¬ max(i + ar0) ⊦ ordered≤(rev(ar0)) ∧ ¬ max(ar0)

Rule argument

Additional information

Used simplifier rules: array freely generated by [], +;;

Proof step 3 from proof descending-order-is-max-permuted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ¬ max([]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ordered≤([]); (s) ⊦ rev([]) = []; (s)

Proof step 4 from proof descending-order-is-max-permuted (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ max(ar1) ↔ (∀ ar2. perm(ar1, ar2) → ar2 ≤ ar1)

• Proof step 6:

  ∃ ar2. ¬(perm([], ar2) → ar2 ≤ []) ⊦

Rule argument

Additional information

Used terms: []

Proof step 5 from proof descending-order-is-max-permuted (previous step) (back to tree)

Lemma maximum-permutation

Proof step 6 from proof descending-order-is-max-permuted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ¬ [] ≤ [] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ perm([], y) ↔ y = []; (s)

Proof step 7 from proof descending-order-is-max-permuted (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ [] ≤ []

Rule argument

Additional information

Used terms:

Proof step 8 from proof descending-order-is-max-permuted (previous step) (back to tree)

Lemma lexicographic-base1

Proof step 9 from proof descending-order-is-max-permuted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  max(ar0), ordered≤(rev(ar0) + i '), ¬ max(i ' + ar0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ordered≤(x + y) → ordered≤(x); (s) ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ x + a = x + a '; (s) ⊦ rev(a ' + x) = rev(x) + a; (s)

Proof step 10 from proof descending-order-is-max-permuted (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ max(ar1) ↔ (∀ ar2. perm(ar1, ar2) → ar2 ≤ ar1)

• Proof step 12:

  max(ar0), ordered≤(rev(ar0) + i '), ∃ ar2. ¬(perm(i ' + ar0, ar2) → ar2 ≤ i ' + ar0) ⊦

Rule argument

Additional information

Used terms: i ' + ar0

Proof step 11 from proof descending-order-is-max-permuted (previous step) (back to tree)

Lemma maximum-permutation

Proof step 12 from proof descending-order-is-max-permuted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  max(ar0), ordered≤(rev(ar0) + i '), perm(i ' + ar0, ar2), ¬ ar2 ≤ i ' + ar0 ⊦

Rule argument

Additional information

Proof step 13 from proof descending-order-is-max-permuted (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 14:

  max(ar0), ordered≤(rev(ar0) + i '), perm(i ' + ar0, i0 + ar), ¬ i0 + ar ≤ i ' + ar0, ∀ ar0, i. ¬(max(ar0) ∧ ordered≤(rev(ar0) + i ') ∧ perm(i ' + ar0, ar) ∧ ¬ ar ≤ i ' + ar0) ⊦

Rule argument

Additional information

Used simplifier rules: array freely generated by [], +;; ⊦ perm(x, []) ↔ x = []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (as) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort]

Proof step 14 from proof descending-order-is-max-permuted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  max(ar0), ordered≤(rev(ar0) + i '), perm(i ' + ar0, i0 ' + ar), ¬ i0 ' + ar ≤ i ' + ar0, ∀ ar1, i1. ¬ max(ar1) ∨ ¬ ordered≤(rev(ar1) + i1 ') ∨ ¬ perm(i1 ' + ar1, ar) ∨ ar ≤ i1 ' + ar1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 15 from proof descending-order-is-max-permuted (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ n ' + ar1 ≤ m ' + ar2 ↔ (n = m ⊃ ar1 ≤ ar2;n ≤ m)

• Proof step 17:

  max(ar0), ordered≤(rev(ar0) + i '), perm(i ' + ar0, i0 ' + ar), (i0 = i ⊃ ¬ ar ≤ ar0;¬ i0 ≤ i), ∀ ar1, i1. ¬ max(ar1) ∨ ¬ ordered≤(rev(ar1) + i1 ') ∨ ¬ perm(i1 ' + ar1, ar) ∨ ar ≤ i1 ' + ar1 ⊦

Rule argument

Additional information

Used terms: i0, ar, i, ar0

Proof step 16 from proof descending-order-is-max-permuted (previous step) (back to tree)

Lemma lexicographic-rec1

Proof step 17 from proof descending-order-is-max-permuted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  max(ar0), ordered≤(rev(ar0) + i '), perm(i ' + ar0, i0 ' + ar), (i0 = i ⊃ ¬ ar ≤ ar0;¬ i0 < i), ∀ ar1, i1. ¬ max(ar1) ∨ ¬ ordered≤(rev(ar1) + i1 ') ∨ ¬ perm(i1 ' + ar1, ar) ∨ ar ≤ i1 ' + ar1 ⊦

Rule argument

Additional information

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

Proof step 18 from proof descending-order-is-max-permuted (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 19:

  i0 = i, max(ar0), ordered≤(rev(ar0) + i '), perm(i ' + ar0, i0 ' + ar), ¬ ar ≤ ar0, ∀ ar1, i1. ¬ max(ar1) ∨ ¬ ordered≤(rev(ar1) + i1 ') ∨ ¬ perm(i1 ' + ar1, ar) ∨ ar ≤ i1 ' + ar1 ⊦

• Proof step 23:

  i0 ≠ i, max(ar0), ordered≤(rev(ar0) + i '), perm(i ' + ar0, i0 ' + ar), ¬ i0 < i, ∀ ar1, i1. ¬ max(ar1) ∨ ¬ ordered≤(rev(ar1) + i1 ') ∨ ¬ perm(i1 ' + ar1, ar) ∨ ar ≤ i1 ' + ar1 ⊦

Rule argument

Additional information

Proof step 19 from proof descending-order-is-max-permuted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  max(ar0), ordered≤(rev(ar0) + i '), perm(ar0, ar), ¬ ar ≤ ar0, ∀ ar1, i1. ¬ max(ar1) ∨ ¬ ordered≤(rev(ar1) + i1 ') ∨ ¬ perm(i1 ' + ar1, ar) ∨ ar ≤ i1 ' + ar1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ perm(a ' + x, a ' + y) ↔ perm(x, y); (s)

Proof step 20 from proof descending-order-is-max-permuted (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ max(ar1) ↔ (∀ ar2. perm(ar1, ar2) → ar2 ≤ ar1)

• Proof step 22:

  ordered≤(rev(ar0) + i '), perm(ar0, ar), ¬ ar ≤ ar0, ∀ ar1, i1. ¬ max(ar1) ∨ ¬ ordered≤(rev(ar1) + i1 ') ∨ ¬ perm(i1 ' + ar1, ar) ∨ ar ≤ i1 ' + ar1, ∀ ar2. perm(ar0, ar2) → ar2 ≤ ar0 ⊦

Rule argument

Additional information

Used terms: ar0

Proof step 21 from proof descending-order-is-max-permuted (previous step) (back to tree)

Lemma maximum-permutation

Proof step 22 from proof descending-order-is-max-permuted (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: ar

Proof step 23 from proof descending-order-is-max-permuted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  i0 ≠ i, i < i0, max(ar0), ordered≤(rev(ar0) + i '), perm(i ' + ar0, i0 ' + ar), ∀ ar1, i1. ¬ max(ar1) ∨ ¬ ordered≤(rev(ar1) + i1 ') ∨ ¬ perm(i1 ' + ar1, ar) ∨ ar ≤ i1 ' + ar1 ⊦

Rule argument

Additional information

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

Proof step 24 from proof descending-order-is-max-permuted (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ a ≠ b → (perm(a ' + x, b ' + y) ↔ a ∈ y ∧ b ∈ x ∧ perm(x -1l b, y -1l a))

• Proof step 26:

  i0 ≠ i, i < i0, max(ar0), ordered≤(rev(ar0) + i '), perm(ar0 -1l i0, ar -1l i), i ∈ ar, i0 ∈ ar0, ∀ ar1, i1. ¬ max(ar1) ∨ ¬ ordered≤(rev(ar1) + i1 ') ∨ ¬ perm(i1 ' + ar1, ar) ∨ ar ≤ i1 ' + ar1 ⊦

Rule argument

Additional information

Used terms: i, ar0, i0, ar

Proof step 25 from proof descending-order-is-max-permuted (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof descending-order-is-max-permuted (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ i > j ∧ i ∈ ar1 ∧ j ∈ ar2 → ¬ ordered≤(ar1 + ar2)

Rule argument

Additional information

Used simplifier rules: ⊦ m > n ↔ n < m; (s) ⊦ a ∈ rev(x) ↔ a ∈ x; (s) ⊦ a ∈ b ' ↔ a = b; (s) Used terms: rev(ar0), i ', i0, i

Proof step 27 from proof descending-order-is-max-permuted (previous step) (back to tree)

Lemma not-ordered