Proof step 1 from proof ins-max (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ins≤(a, x0) ≠ x0 + a ', ordered≤(x0), ¬ a < max(x0) ⊦

Rule argument

Additional information

Proof step 2 from proof ins-max (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ins≤(a, x0) ≠ x0 + a ', ordered≤(x0), ¬ a < max(x0) ⊦

Rule argument

Additional information

Proof step 3 from proof ins-max (previous step) (back to tree)

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 4:

  ins≤(a, a0 + x) ≠ (a0 + x) + a ', ordered≤(a0 + x), ¬ a < max(a0 + x), ∀ a. ¬(ins≤(a, x) ≠ x + a ' ∧ ordered≤(x) ∧ ¬ a < max(x)) ⊦

Rule argument

Additional information

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

Proof step 4 from proof ins-max (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ins≤(a, a0 ' + x) ≠ (a0 ' + x) + a ', ordered≤(a0 ' + x), ¬ a < max(a0 ' + x), ∀ a1. ins≤(a1, x) = x + a1 ' ∨ a1 < max(x) ⊦

Rule argument

Additional information

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

Proof step 5 from proof ins-max (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ ordered≤(a ' + x) → ins≤(a, x) = a ' + x

• Proof step 7:

  ins≤(a, a0 ' + x) ≠ (a0 ' + x) + a ', ordered≤(a0 ' + x), ¬ a < max(a0 ' + x), ¬ ordered≤(a ' + a0 ' + x), ∀ a1. ins≤(a1, x) = x + a1 ' ∨ a1 < max(x) ⊦

• Proof step 12:

  a ' + a0 ' + x ≠ (a0 ' + x) + a ', ordered≤(a0 ' + x), ordered≤(a ' + a0 ' + x), ¬ a < max(a0 ' + x), ∀ a1. ins≤(a1, x) = x + a1 ' ∨ a1 < max(x) ⊦

Rule argument

Additional information

Used terms: a, a0 ' + x

Proof step 6 from proof ins-max (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof ins-max (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ins≤(a, x) ≠ x + a ', a0 < a, ordered≤(a0 ' + x), ¬ a < max(a0 ' + x), ∀ a1. ins≤(a1, x) = x + a1 ' ∨ a1 < max(x) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ a + x = a ' + x; (s) ⊦ b < a → ins≤(a, b ' + x) = b + ins≤(a, x); (s) ⊦ ordered≤(a ' + b ' + x) ↔ ¬ b < a ∧ ordered≤(b ' + x); (ws)

Proof step 8 from proof ins-max (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 9:

  ins≤(a, x) ≠ x + a ', a0 < a, ordered≤(a0 ' + x), ¬ a < max(a0 ' + x), ∀ a1. ins≤(a1, x) = x + a1 ' ∨ a1 < max(x), ins≤(a, x) = x + a ' ∨ a < max(x) ⊦

Rule argument

Additional information

Used terms: a

Proof step 9 from proof ins-max (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ins≤(a, x) ≠ x + a ', a0 < a, a < max(x), max(a0 ' + x) < max(x), a0 < max(x), ordered≤(a0 ' + x), ¬ a < max(a0 ' + x), ∀ a1. ins≤(a1, x) = x + a1 ' ∨ a1 < max(x) ⊦

Rule argument

Additional information

Used simplifier rules: nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification oelem transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification oelem

Proof step 10 from proof ins-max (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ x ≠ [] → max(a ' + x) = (max(x) < a ⊃ a;max(x))

Rule argument

Additional information

Used simplifier rules: ⊦ a < b → (b < a ↔ false); (ss) ⊦ ins≤(a, []) = a '; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' = b ' ↔ a = b; (s) Used terms: a0, x

Proof step 11 from proof ins-max (previous step) (back to tree)

Lemma max-rec

Proof step 12 from proof ins-max (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  a ' + a0 ' + x ≠ (a0 ' + x) + a ', ordered≤(a0 ' + x), ¬ a < max(a0 ' + x), ¬ a0 < a, ¬ a0 < max(a0 ' + x), ∀ a1. ins≤(a1, x) = x + a1 ' ∨ a1 < max(x) ⊦

Rule argument

Additional information

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

Proof step 13 from proof ins-max (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ x ≠ [] → max(a ' + x) = (max(x) < a ⊃ a;max(x))

• Proof step 15:

  a ' + a0 ' + x ≠ (a0 ' + x) + a ', x ≠ [], ordered≤(a0 ' + x), ¬ a < (max(x) < a0 ⊃ a0;max(x)), ¬ a0 < a, ¬ a0 < (max(x) < a0 ⊃ a0;max(x)), ∀ a1. ins≤(a1, x) = x + a1 ' ∨ a1 < max(x) ⊦

Rule argument

Additional information

Used simplifier rules: max-base: ⊦ max(a ') = a; ⊦ [] + x = x; (s) ⊦ ordered≤(a '); (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ b < a → (a < b ↔ a ≠ b); (ss) Used terms: a0, x

Proof step 14 from proof ins-max (previous step) (back to tree)

Lemma max-rec

Proof step 15 from proof ins-max (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  a ' + a0 ' + x ≠ (a0 ' + x) + a ', x ≠ [], ordered≤(a0 ' + x), ¬ a < (max(x) < a0 ⊃ a0;max(x)), ¬ a0 < a, ¬ a0 < (max(x) < a0 ⊃ a0;max(x)), ∀ a1. ins≤(a1, x) = x + a1 ' ∨ a1 < max(x) ⊦

Rule argument

Additional information

Used simplifier rules: nnn: ⊦ ¬ c < b ∧ ¬ a < c → ¬ a < b; (forward) from specification oelem

Proof step 16 from proof ins-max (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 17:

  a ' + a0 ' + x ≠ (a0 ' + x) + a ', x ≠ [], max(x) < a0, ordered≤(a0 ' + x), ¬ a0 < a0, ¬ a < (max(x) < a0 ⊃ a0;max(x)), ¬ a0 < a, ∀ a1. ins≤(a1, x) = x + a1 ' ∨ a1 < max(x) ⊦

• Proof step 19:

  a ' + a0 ' + x ≠ (a0 ' + x) + a ', x ≠ [], ordered≤(a0 ' + x), ¬ max(x) < a0, ¬ a0 < max(x), ¬ a < (max(x) < a0 ⊃ a0;max(x)), ¬ a0 < a, ∀ a1. ins≤(a1, x) = x + a1 ' ∨ a1 < max(x) ⊦

Rule argument

Additional information

Proof step 17 from proof ins-max (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  a0 ' + x ≠ x + a0 ', x ≠ [], max(x) < a0, ordered≤(a0 ' + x), ∀ a1. ins≤(a1, x) = x + a1 ' ∨ a1 < max(x) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a < a; (s) ⊦ ¬ b < a → (a < b ↔ a ≠ b); (ss) nen: ⊦ ¬ b < a ∧ a = c → ¬ b < c; (forward) from specification oelem a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' + x = b ' + y ↔ a = b ∧ x = y; (ws)

Proof step 18 from proof ins-max (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 ⊦ ordered≤(a ' + x) → ins≤(a, x) = a ' + x; (s) transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification oelem ⊦ ¬ a < a; (s) Used terms: a0

Proof step 19 from proof ins-max (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  max(x) ' + x ≠ x + max(x) ', x ≠ [], ordered≤(max(x) ' + x), ∀ a1. ins≤(a1, x) = x + a1 ' ∨ a1 < max(x) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a < a; (s) ⊦ ¬ b < a → (a < b ↔ a ≠ b); (ss) nen: ⊦ ¬ b < a ∧ a = c → ¬ b < c; (forward) from specification oelem a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' + x = b ' + y ↔ a = b ∧ x = y; (ws)

Proof step 20 from proof ins-max (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 ⊦ ordered≤(a ' + x) → ins≤(a, x) = a ' + x; (s) ⊦ ¬ a < a; (s) Used terms: max(x)