Proof step 1 from proof ole-last (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(ordered≤(x + a ' + b ') ↔ ¬ b < a), ordered≤(x + a ') ⊦

Rule argument

Additional information

Proof step 2 from proof ole-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(ordered≤(x + a ' + b ') ↔ ¬ b < a), ordered≤(x + a ') ⊦

Rule argument

Additional information

Proof step 3 from proof ole-last (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  ¬(ordered≤((a0 + x0) + a ' + b ') ↔ ¬ b < a), ordered≤((a0 + x0) + a '), ∀ a, b. ¬(¬(ordered≤(x0 + a ' + b ') ↔ ¬ b < a) ∧ ordered≤(x0 + a ')) ⊦

Rule argument

Additional information

Used simplifier rules: ole-two: ⊦ ordered≤(a ' + b ') ↔ ¬ b < a; list freely generated by [], +;; ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 4 from proof ole-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ¬(ordered≤((a0 ' + x0) + a ' + b ') ↔ ¬ b < a), ordered≤((a0 ' + x0) + a '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 ') ⊦

Rule argument

Additional information

Used simplifier rules: cons-02: ⊦ ordered≤(a ' + x) → ordered≤(x); app-01: ⊦ ordered≤(x + y) → ordered≤(y); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s)

Proof step 5 from proof ole-last (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 6:

  ¬(ordered≤((a0 ' + x0) + a ' + b ') ↔ ¬ b < a), b < a, ordered≤((a0 ' + x0) + a '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 ') ⊦

• Proof step 8:

  ¬(ordered≤((a0 ' + x0) + a ' + b ') ↔ ¬ b < a), ordered≤((a0 ' + x0) + a '), ¬ b < a, ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 ') ⊦

Rule argument

Additional information

Used formulas: b < a

Proof step 6 from proof ole-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  b < a, ordered≤((a0 ' + x0) + a ' + b '), ordered≤((a0 ' + x0) + a '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 ') ⊦

Rule argument

Additional information

Used simplifier rules: cons-02: ⊦ ordered≤(a ' + x) → ordered≤(x); app-01: ⊦ ordered≤(x + y) → ordered≤(y); a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 7 from proof ole-last (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: app-01: ⊦ ordered≤(x + y) → ordered≤(y); a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a, b

Proof step 8 from proof ole-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ordered≤((a0 ' + x0) + a '), ¬ b < a, ¬ ordered≤((a0 ' + x0) + a ' + b '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 ') ⊦

Rule argument

Additional information

Proof step 9 from proof ole-last (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ x ≠ [] ∧ x.tail ≠ [] → (ordered≤(x) ↔ ¬ x.tail.head < x.head ∧ ordered≤(x.tail))

• Proof step 11:

  (a0 ' + x0) + a ' ≠ [], ((a0 ' + x0) + a ').tail ≠ [], ordered≤(((a0 ' + x0) + a ').tail), ¬ ((a0 ' + x0) + a ').tail.head < ((a0 ' + x0) + a ').head, ¬ b < a, ¬ ordered≤((a0 ' + x0) + a ' + b '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 ') ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ' + x ≠ []; (s) ⊦ (a ' + x).tail = x; (s) ⊦ x + a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: (a0 ' + x0) + a '

Proof step 10 from proof ole-last (previous step) (back to tree)

Lemma ole-rec

Proof step 11 from proof ole-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ordered≤(x0 + a '), ¬ b < a, ¬ (x0 + a ').head < a0, ¬ ordered≤((a0 ' + x0) + a ' + b '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 ') ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).head = a; (s) ⊦ (a ' + x).tail = x; (s) ⊦ x + a ' ≠ []; (s) ⊦ a ' + x ≠ []; (s)

Proof step 12 from proof ole-last (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 13:

  x0 + a ' = a2 + y, x0 + a ' ≠ [], ordered≤(x0 + a '), ¬ b < a, ¬ a2 < a0, ¬ ordered≤((a0 ' + x0) + a ' + b '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 ') ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x + y = [] ↔ x = [] ∧ y = []; (as) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x0 + a ', a2, y

Proof step 13 from proof ole-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  x0 + a ' = a2 ' + y, ordered≤(a2 ' + y), ¬ a2 < a0, ¬ b < a, ¬ ordered≤((a0 ' + x0) + a ' + b '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 '), a = a2 ∨ a ∈ y, a2 ∈ x0 ∨ a2 = a ⊦

Rule argument

Additional information

Used simplifier rules: cons-02: ⊦ ordered≤(a ' + x) → ordered≤(x); app-01: ⊦ ordered≤(x + y) → ordered≤(y); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ b ' ↔ a = b; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ x + a ' ≠ []; (s) ⊦ a + x = a ' + x; (s)

Proof step 14 from proof ole-last (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 15:

  x0 + a ' = a2 ' + y, ordered≤(a2 ' + y), a ∈ y, ¬ a2 < a0, ¬ b < a, ¬ ordered≤((a0 ' + x0) + a ' + b '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 '), a2 ∈ x0 ∨ a2 = a, a = a2 ∨ a ∈ y ⊦

Rule argument

Additional information

Used simplifier rules: le-o: ⊦ ordered≤(a '); le-r: ⊦ ordered≤(a ' + b ' + x) ↔ ¬ b < a ∧ ordered≤(b ' + x); ole-two: ⊦ ordered≤(a ' + b ') ↔ ¬ b < a; ni: ⊦ x + a ' = y + z ∧ ¬ a ∈ z → z = []; (forward) from specification list nen: ⊦ ¬ b < a ∧ a = c → ¬ b < c; (forward) from specification oelem ⊦ a ' = x + b ' ↔ a = b ∧ x = []; (ws) ⊦ x + [] = x; (s) ⊦ ¬ a ∈ []; (s) nnn: ⊦ ¬ c < b ∧ ¬ a < c → ¬ a < b; (forward) from specification oelem ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used formulas: a ∈ y

Proof step 15 from proof ole-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  x0 + a ' = a2 ' + y, ordered≤(a2 ' + y), a ∈ y, ¬ b < a2, ¬ a < a0, ¬ a2 < a0, ¬ b < a, ¬ a < a2, ¬ b < a0, ¬ ordered≤((a0 ' + x0) + a ' + b '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 '), a2 ∈ x0 ∨ a2 = a ⊦

Rule argument

Additional information

Used simplifier rules: ole-in: ⊦ ordered≤(a ' + x) ∧ b ∈ x → ¬ b < a; nnn: ⊦ ¬ c < b ∧ ¬ a < c → ¬ a < b; (forward) from specification oelem a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 16 from proof ole-last (previous step) (back to tree)

Heuristic cut applied rule cut formula

And obtained the following new goals

• Proof step 17:

  x0 + a ' = a2 ' + y, a2 = a, ordered≤(a2 ' + y), a ∈ y, ¬ b < a2, ¬ a < a0, ¬ a2 < a0, ¬ b < a, ¬ a < a2, ¬ b < a0, ¬ ordered≤((a0 ' + x0) + a ' + b '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 '), a2 ∈ x0 ∨ a2 = a ⊦

• Proof step 22:

  x0 + a ' = a2 ' + y, a2 ≠ a, ordered≤(a2 ' + y), a ∈ y, ¬ b < a2, ¬ a < a0, ¬ a2 < a0, ¬ b < a, ¬ a < a2, ¬ b < a0, ¬ ordered≤((a0 ' + x0) + a ' + b '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 '), a2 ∈ x0 ∨ a2 = a ⊦

Rule argument

Additional information

Used formulas: a2 = a

Proof step 17 from proof ole-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  x0 + a ' = a ' + y, ordered≤(a ' + y), a ∈ y, ¬ b < a0, ¬ a < a0, ¬ b < a, ¬ ordered≤((a0 ' + x0) + a ' + b '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 ') ⊦

Rule argument

Additional information

Used simplifier rules: ole-in: ⊦ ordered≤(a ' + x) ∧ b ∈ x → ¬ b < a; ⊦ ¬ a < a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ b ' ↔ a = b; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ y → a ∈ x + y; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list

Proof step 18 from proof ole-last (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ x ≠ [] ∧ x.tail ≠ [] → (ordered≤(x) ↔ ¬ x.tail.head < x.head ∧ ordered≤(x.tail))

• Proof step 20:

  x0 + a ' = a ' + y, (a0 ' + x0) + a ' + b ' ≠ [], ((a0 ' + x0) + a ' + b ').tail ≠ [], ordered≤(a ' + y), a ∈ y, ¬ b < a0, ¬ a < a0, ¬ b < a, ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 '), ((a0 ' + x0) + a ' + b ').tail.head < ((a0 ' + x0) + a ' + b ').head ∨ ¬ ordered≤(((a0 ' + x0) + a ' + b ').tail) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ' + x ≠ []; (s) ⊦ (a ' + x).tail = x; (s) ⊦ x + a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: (a0 ' + x0) + a ' + b '

Proof step 19 from proof ole-last (previous step) (back to tree)

Lemma ole-rec

Proof step 20 from proof ole-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  x0 + a ' = a ' + y, ordered≤(a ' + y), a ∈ y, ¬ b < a, ¬ a < a0, ¬ b < a0, ¬ ordered≤(x0 + a ' + b '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 ') ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).head = a; (s) ⊦ (a ' + x).tail = x; (s) ⊦ (x + a ' + y).head = (x + a ').head; (s) ⊦ x + a ' ≠ []; (s) ⊦ a ' + x ≠ []; (s)

Proof step 21 from proof ole-last (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a, b

Proof step 22 from proof ole-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  x0 + y.last ' = a2 ' + y, a2 ≠ y.last, y ≠ [], a0 < y.last, a2 < y.last, ordered≤(a2 ' + y), a2 ∈ x0, ¬ b < a0, ¬ b < a2, ¬ a2 < a0, ¬ b < y.last, ¬ ordered≤((a0 ' + x0) + y.last ' + b '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 ') ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ x → a ∈ x + y; (s) ⊦ x.last ∈ x ↔ x ≠ []; (s) ⊦ a ≠ b → (a ∈ b ' + x ↔ a ∈ x); (s) nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification oelem in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list inapp-10: ⊦ a ' + x = y + b ' ∧ a ≠ b → a ∈ y ∧ b ∈ x; (forward) from specification list lapp-04: ⊦ a ' + x = y + b ' ∧ a ≠ b → x.last = b; (forward) from specification list-last ⊦ a < b → (b < a ↔ false); (ss) ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss)

Proof step 23 from proof ole-last (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 24:

  x0 + a ' = a2 ' + y, y = y0 + a ', a2 ≠ a, y ≠ [], a2 < a, a0 < a, ordered≤(a2 ' + y), a2 ∈ x0, ¬ b < a0, ¬ b < a2, ¬ a2 < a0, ¬ b < a, ¬ ordered≤((a0 ' + x0) + a ' + b '), ∀ a1, b0. (ordered≤(x0 + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤(x0 + a1 ') ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: y, a, y0

Proof step 24 from proof ole-last (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  a2 ≠ a, a0 < a, a2 < a, ordered≤(a2 ' + y0 + a '), ¬ b < a, ¬ a2 < a0, ¬ b < a2, ¬ b < a0, ¬ ordered≤(a2 ' + y0 + a ' + b '), ∀ a1, b0. (ordered≤((a2 ' + y0) + a1 ' + b0 ') ↔ ¬ b0 < a1) ∨ ¬ ordered≤((a2 ' + y0) + a1 ') ⊦

Rule argument

Additional information

Used simplifier rules: cons-02: ⊦ ordered≤(a ' + x) → ordered≤(x); app-01: ⊦ ordered≤(x + y) → ordered≤(y); le-r: ⊦ ordered≤(a ' + b ' + x) ↔ ¬ b < a ∧ ordered≤(b ' + x); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ b ' + x ↔ a = b ∨ a ∈ x; (s) nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification oelem in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ x + a ' ≠ []; (s) ⊦ # y = # y0 → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws)

Proof step 25 from proof ole-last (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a, b