Proof step 1 from proof orderedls-le-attach (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof orderedls-le-attach (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: list('a) freely generated by [], +;; ⊦ ¬ a ∈ []; (s)

Proof step 3 from proof orderedls-le-attach (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s)

Proof step 4 from proof orderedls-le-attach (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

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

Rule argument

Additional information

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

Proof step 5 from proof orderedls-le-attach (previous step) (back to tree)

Lemma ols-rec

Proof step 6 from proof orderedls-le-attach (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

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

Proof step 7 from proof orderedls-le-attach (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

Used simplifier rules: ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ 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 8 from proof orderedls-le-attach (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ 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 ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a + x = a ' + x; (s)

Proof step 9 from proof orderedls-le-attach (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

Proof step 10 from proof orderedls-le-attach (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: orderedls-ls: ⊦ b < a ∧ b ∈ x → ¬ ordered<(a ' + x); lel: ⊦ a < b ∧ a = c → c < b; (forward) from specification weakord[tord] nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification weakord[tord] a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a, b