Proof step 1 from proof del1-01 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ordered≤(x), ¬ ordered≤(x -1l a) ⊦

Rule argument

Additional information

Proof step 2 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ordered≤(x), ¬ ordered≤(x -1l a) ⊦

Rule argument

Additional information

Proof step 3 from proof del1-01 (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  ordered≤(a0 + x0), ¬ ordered≤((a0 + x0) -1l a), ∀ a. ¬(ordered≤(x0) ∧ ¬ ordered≤(x0 -1l a)) ⊦

Rule argument

Additional information

Used simplifier rules: le-e: ⊦ ordered≤([]); list('a) freely generated by [], +;; ⊦ [] -1l a = []; (s)

Proof step 4 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ordered≤(x0), ordered≤(a0 ' + x0), ¬ ordered≤((a0 ' + x0) -1l a), ∀ a1. ordered≤(x0 -1l a1) ⊦

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)

Proof step 5 from proof del1-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ a ≠ b → (b ' + x) -1l a = b ' + (x -1l a)

• Proof step 7:

  a ≠ a0, ordered≤(a0 ' + x0), ordered≤(x0), ¬ ordered≤(a0 ' + (x0 -1l a)), ∀ a1. ordered≤(x0 -1l a1) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (a ' + x) -1l a = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a, a0, x0

Proof step 6 from proof del1-01 (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  a ≠ a0, ordered≤(x0), ordered≤(a0 ' + x0), ¬ ordered≤(a0 ' + (x0 -1l a)), ∀ a1. ordered≤(x0 -1l a1) ⊦

Rule argument

Additional information

Proof step 8 from proof del1-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  a0 ' + x0 ≠ [], (a0 ' + x0).tail ≠ [], a ≠ a0, ordered≤((a0 ' + x0).tail), ordered≤(x0), ¬ (a0 ' + x0).tail.head < (a0 ' + x0).head, ¬ ordered≤(a0 ' + (x0 -1l a)), ∀ a1. ordered≤(x0 -1l a1) ⊦

Rule argument

Additional information

Used simplifier rules: le-e: ⊦ ordered≤([]); le-o: ⊦ ordered≤(a '); ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ (a ' + x).tail = x; (s) ⊦ [] -1l a = []; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a0 ' + x0

Proof step 9 from proof del1-01 (previous step) (back to tree)

Lemma ole-rec

Proof step 10 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  a ≠ a0, x0 ≠ [], ordered≤(x0), ¬ x0.head < a0, ¬ ordered≤(a0 ' + (x0 -1l a)), ∀ a1. ordered≤(x0 -1l 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) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 11 from proof del1-01 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  x0 = a2 + y, a ≠ a0, x0 ≠ [], ordered≤(x0), ¬ a2 < a0, ¬ ordered≤(a0 ' + (x0 -1l a)), ∀ a1. ordered≤(x0 -1l a1) ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: x0, a2, y

Proof step 12 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  a ≠ a0, ordered≤(a2 ' + y), ordered≤(y), ¬ a2 < a0, ¬ ordered≤(a0 ' + ((a2 ' + y) -1l a)), ∀ a1. ordered≤((a2 ' + y) -1l a1) ⊦

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 13 from proof del1-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  a0 ' + ((a2 ' + y) -1l a) ≠ [], (a0 ' + ((a2 ' + y) -1l a)).tail ≠ [], a ≠ a0, ordered≤(y), ordered≤(a2 ' + y), ¬ a2 < a0, ∀ a1. ordered≤((a2 ' + y) -1l a1), (a0 ' + ((a2 ' + y) -1l a)).tail.head < (a0 ' + ((a2 ' + y) -1l a)).head ∨ ¬ ordered≤((a0 ' + ((a2 ' + y) -1l a)).tail) ⊦

Rule argument

Additional information

Used simplifier rules: le-o: ⊦ ordered≤(a '); ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ (a ' + x).tail = x; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a0 ' + ((a2 ' + y) -1l a)

Proof step 14 from proof del1-01 (previous step) (back to tree)

Lemma ole-rec

Proof step 15 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  (a2 ' + y) -1l a ≠ [], a ≠ a0, ordered≤(a2 ' + y), ordered≤(y), ¬ a2 < a0, ∀ a1. ordered≤((a2 ' + y) -1l a1), ((a2 ' + y) -1l a).head < a0 ∨ ¬ ordered≤((a2 ' + y) -1l a) ⊦

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 16 from proof del1-01 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  (a2 ' + y) -1l a = a3 + y0, (a2 ' + y) -1l a ≠ [], a ≠ a0, ordered≤(y), ordered≤(a2 ' + y), ¬ a2 < a0, ∀ a1. ordered≤((a2 ' + y) -1l a1), a3 < a0 ∨ ¬ ordered≤((a2 ' + y) -1l a) ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: (a2 ' + y) -1l a, a3, y0

Proof step 17 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  (a2 ' + y) -1l a = a3 ' + y0, a ≠ a0, ordered≤(a2 ' + y), ordered≤(y), ¬ a2 < a0, ∀ a1. ordered≤((a2 ' + y) -1l a1), a3 < a0 ∨ ¬ ordered≤(a3 ' + y0) ⊦

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 ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s)

Proof step 18 from proof del1-01 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 19:

  (a2 ' + y) -1l a = a3 ' + y0, a ≠ a0, ordered≤(y), ordered≤(a2 ' + y), ordered≤((a2 ' + y) -1l a), ¬ a2 < a0, ∀ a1. ordered≤((a2 ' + y) -1l a1), a3 < a0 ∨ ¬ ordered≤(a3 ' + y0) ⊦

Rule argument

Additional information

Used terms: a

Proof step 19 from proof del1-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  (a2 ' + y) -1l a = a3 ' + y0, a ≠ a0, a3 < a0, ordered≤(y0), ordered≤(y), ordered≤(a2 ' + y), ordered≤(a3 ' + y0), ¬ a2 < a0, ∀ a1. ordered≤((a2 ' + y) -1l a1) ⊦

Rule argument

Additional information

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

Proof step 20 from proof del1-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ a ≠ b → (b ' + x) -1l a = b ' + (x -1l a)

Rule argument

Additional information

Used simplifier rules: le-r: ⊦ ordered≤(a ' + b ' + x) ↔ ¬ b < a ∧ ordered≤(b ' + x); ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x) -1l a = x; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification weakord leq-trans: ⊦ ¬ b < a ∧ ¬ c < b → ¬ c < a; (forward) from specification weakord Used terms: a, a2, y

Proof step 21 from proof del1-01 (previous step) (back to tree)

A spec-lemma