Proof step 1 from proof orderedle-append (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ordered≤(x), ordered≤(x0), ¬ ordered≤(x + x0), x ≠ [] ∧ x0 ≠ [] → ¬ x0.head < x.last ⊦

Rule argument

Additional information

Proof step 2 from proof orderedle-append (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ordered≤(x0), ordered≤(x), ¬ ordered≤(x + x0), x ≠ [] ∧ x0 ≠ [] → ¬ x0.head < x.last ⊦

Rule argument

Additional information

Proof step 3 from proof orderedle-append (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  ordered≤(a + x1), ordered≤(x0), ¬ ordered≤((a + x1) + x0), a + x1 ≠ [] ∧ x0 ≠ [] → ¬ x0.head < (a + x1).last, ∀ x0. ¬(ordered≤(x0) ∧ ordered≤(x1) ∧ ¬ ordered≤(x1 + x0) ∧ (x1 ≠ [] ∧ x0 ≠ [] → ¬ x0.head < x1.last)) ⊦

Rule argument

Additional information

Used simplifier rules: le-e: ⊦ ordered≤([]); list('a) freely generated by [], +;; ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 4 from proof orderedle-append (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ordered≤(x1), ordered≤(a ' + x1), ordered≤(x0), ¬ ordered≤((a ' + x1) + x0), x0 ≠ [] → ¬ x0.head < (a ' + x1).last, ∀ x. ¬ ordered≤(x) ∨ ordered≤(x1 + x) ∨ ¬(x1 ≠ [] ∧ x ≠ [] → ¬ x.head < x1.last) ⊦

Rule argument

Additional information

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

Proof step 5 from proof orderedle-append (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  x0 = a0 + y, x0 ≠ [], ordered≤(x0), ordered≤(a ' + x1), ordered≤(x1), ¬ ordered≤((a ' + x1) + x0), x0 ≠ [] → ¬ a0 < (a ' + x1).last, ∀ x. ¬ ordered≤(x) ∨ ordered≤(x1 + x) ∨ ¬(x1 ≠ [] ∧ x ≠ [] → ¬ x.head < x1.last) ⊦

Rule argument

Additional information

Used simplifier rules: le-e: ⊦ ordered≤([]); ⊦ x + [] = x; (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, a0, y

Proof step 6 from proof orderedle-append (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ordered≤(x1), ordered≤(a ' + x1), ordered≤(a0 ' + y), ordered≤(y), ¬ a0 < (a ' + x1).last, ¬ ordered≤(a ' + x1 + a0 ' + y), ∀ x. ¬ ordered≤(x) ∨ ordered≤(x1 + x) ∨ ¬(x1 ≠ [] ∧ x ≠ [] → ¬ x.head < x1.last) ⊦

Rule argument

Additional information

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

Proof step 7 from proof orderedle-append (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 8:

  x1 ≠ [], ordered≤(y), ordered≤(a0 ' + y), ordered≤(a ' + x1), ordered≤(x1), ¬ a0 < (a ' + x1).last, ¬ ordered≤(a ' + x1 + a0 ' + y), ∀ x. ¬ ordered≤(x) ∨ ordered≤(x1 + x) ∨ ¬(x1 ≠ [] ∧ x ≠ [] → ¬ x.head < x1.last) ⊦

Rule argument

Additional information

Used simplifier rules: le-e: ⊦ ordered≤([]); le-o: ⊦ ordered≤(a '); le-r: ⊦ ordered≤(a ' + b ' + x) ↔ ¬ b < a ∧ ordered≤(b ' + x); ⊦ x + [] = x; (s) ⊦ a '.last = a; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used formulas: x1 = []

Proof step 8 from proof orderedle-append (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  x1 ≠ [], ordered≤(x1), ordered≤(a ' + x1), ordered≤(a0 ' + y), ordered≤(y), ¬ a0 < x1.last, ¬ ordered≤(a ' + x1 + a0 ' + y), ∀ x. ¬ ordered≤(x) ∨ ordered≤(x1 + x) ∨ ¬(x ≠ [] → ¬ x.head < x1.last) ⊦

Rule argument

Additional information

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

Proof step 9 from proof orderedle-append (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 10:

  x1 ≠ [], ordered≤(y), ordered≤(a0 ' + y), ordered≤(a ' + x1), ordered≤(x1), ¬ a0 < x1.last, ¬ ordered≤(a ' + x1 + a0 ' + y), ∀ x. ¬ ordered≤(x) ∨ ordered≤(x1 + x) ∨ ¬(x ≠ [] → ¬ x.head < x1.last), ¬ ordered≤(a0 ' + y) ∨ ordered≤(x1 + a0 ' + y) ∨ ¬(a0 ' + y ≠ [] → ¬ (a0 ' + y).head < x1.last) ⊦

Rule argument

Additional information

Used terms: a0 ' + y

Proof step 10 from proof orderedle-append (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  x1 ≠ [], ordered≤(a ' + x1), ordered≤(a0 ' + y), ordered≤(y), ordered≤(x1 + a0 ' + y), ¬ a0 < x1.last, ¬ ordered≤(a ' + x1 + a0 ' + y), ∀ x. ¬ ordered≤(x) ∨ ordered≤(x1 + x) ∨ ¬(x ≠ [] → ¬ x.head < x1.last) ⊦

Rule argument

Additional information

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

Proof step 11 from proof orderedle-append (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ ordered≤(y) ↔ # y ≤ 1 ∨ ¬ y.tail.head < y.head ∧ ordered≤(y.tail)

• Proof step 13:

  x1 ≠ [], ordered≤(x1 + a0 ' + y), ordered≤(y), ordered≤(a0 ' + y), ordered≤(a ' + x1), ¬ a0 < x1.last, ¬ #(a ' + x1 + a0 ' + y) ≤ 1, ∀ x. ¬ ordered≤(x) ∨ ordered≤(x1 + x) ∨ ¬(x ≠ [] → ¬ x.head < x1.last), (a ' + x1 + a0 ' + y).tail.head < (a ' + x1 + a0 ' + y).head ∨ ¬ ordered≤((a ' + x1 + a0 ' + y).tail) ⊦

Rule argument

Additional information

Used terms: a ' + x1 + a0 ' + y

Proof step 12 from proof orderedle-append (previous step) (back to tree)

Lemma k-le-r

Proof step 13 from proof orderedle-append (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  x1 ≠ [], x1.head < a, ordered≤(a ' + x1), ordered≤(a0 ' + y), ordered≤(y), ordered≤(x1 + a0 ' + y), ¬ a0 < x1.last, ∀ x. ¬ ordered≤(x) ∨ ordered≤(x1 + x) ∨ ¬(x ≠ [] → ¬ x.head < x1.last) ⊦

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) ⊦ x ≠ [] → (x + y).head = x.head; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic n0 < n ⊦ ¬ m + (* n) ≤ (* n0); (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ #(x + y) = # x + # y; (s)

Proof step 14 from proof orderedle-append (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: le-r: ⊦ ordered≤(a ' + b ' + x) ↔ ¬ b < a ∧ ordered≤(b ' + x); ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x1, a1, y0