Proof step 1 from proof ordered-sublist2 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ordered<(x + y + z), ¬ ordered<(x + z) ⊦

Rule argument

Additional information

Proof step 2 from proof ordered-sublist2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ x ≠ [] ∧ y ≠ [] → (ordered<(x + y) ↔ ordered<(x) ∧ ordered<(y) ∧ x.last < y.head)

• Proof step 4:

  y + z ≠ [], x ≠ [], x.last < (y + z).head, ordered<(x), ordered<(y + z), ¬ ordered<(x + z) ⊦

Rule argument

Additional information

Used simplifier rules: ordered-append-second: ⊦ ordered<(x + y) → ordered<(y); ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ [] + x = x; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: x, y + z

Proof step 3 from proof ordered-sublist2 (previous step) (back to tree)

Lemma ordered-append

Proof step 4 from proof ordered-sublist2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  x ≠ [], x.last < (y + z).head, ordered<(y + z), ordered<(x), ¬ ordered<(x + z) ⊦ y = [] ∧ z = []

Rule argument

Additional information

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

Proof step 5 from proof ordered-sublist2 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  y + z = a + y0, y + z ≠ [], x ≠ [], x.last < a, ordered<(x), ordered<(y + z), ¬ ordered<(x + z) ⊦ y = [] ∧ z = []

Rule argument

Additional information

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

Proof step 6 from proof ordered-sublist2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  y + z = a ' + y0, x ≠ [], z ≠ [], x.last < a, z.head < a, ordered<(x), ordered<(y + z), ¬ x.last < z.head, a ∈ y ∨ a ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: ordered-append: ⊦ x ≠ [] ∧ y ≠ [] → (ordered<(x + y) ↔ ordered<(x) ∧ ordered<(y) ∧ x.last < y.head); ordered-append-second: ⊦ ordered<(x + y) → ordered<(y); nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification weakord[tord] a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ x + [] = x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a + x = a ' + x; (s)

Proof step 7 from proof ordered-sublist2 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 8:

  y + z = a ' + y0, z = a0 + x0, x ≠ [], z ≠ [], a0 < a, x.last < a, ordered<(y + z), ordered<(x), ¬ x.last < a0, a ∈ y ∨ a ∈ z ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: z, a0, x0

Proof step 8 from proof ordered-sublist2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  y + a0 ' + x0 = a ' + y0, x ≠ [], a0 < a, x.last < a, ordered<(a ' + y0), ordered<(x), a ∈ y, ¬ x.last < a0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a < a; (s) nen: ⊦ ¬ b < a ∧ a = c → ¬ b < c; (forward) from specification weakord[tord] lel: ⊦ a < b ∧ a = c → c < b; (forward) from specification weakord[tord] a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ a ∈ y → (y + a0 ' + z = a ' + z0 ↔ y = [] ∧ a0 = a ∧ z = z0); (ws) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification weakord[tord] in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 9 from proof ordered-sublist2 (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 10:

  y + a0 ' + x0 = a ' + y0, y = a1 + y1, x ≠ [], x.last < a, a0 < a, ordered<(x), ordered<(a ' + y0), a ∈ y, ¬ x.last < a0 ⊦

Rule argument

Additional information

Used simplifier rules: list('a) freely generated by [], +;; ⊦ [] + x = x; (s) ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 10 from proof ordered-sublist2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  x ≠ [], x.last < a, a0 < a, ordered<(x), ordered<(a ' + y1 + a0 ' + x0), ¬ x.last < a0 ⊦

Rule argument

Additional information

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

Proof step 11 from proof ordered-sublist2 (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  x = y + a1 ', x ≠ [], a0 < a, a1 < a, ordered<(a ' + y1 + a0 ' + x0), ordered<(x), ¬ a1 < a0 ⊦

Rule argument

Additional information

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

Proof step 12 from proof ordered-sublist2 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  a1 < a, a0 < a, ordered<(y + a1 '), ordered<(a ' + y1 + a0 ' + x0), ¬ a1 < a0 ⊦

Rule argument

Additional information

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

Proof step 13 from proof ordered-sublist2 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] Used terms: a0, a, y1 + a0 ' + x0

Proof step 14 from proof ordered-sublist2 (previous step) (back to tree)

Lemma orderedls-le