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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  x + x0 ≠ [], ¬(max(x + x0) = max(x0 + x) ↔ true) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  x + x0 ≠ [], max(x + x0) ≠ max(x0 + x) ⊦

Rule argument

Additional information

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

User applied rule induction

And obtained the following new goals

• Proof step 4:

  x + x0 ≠ [], max(x + x0) ≠ max(x0 + x), ∀ x1, x2. # x1 + # x2 < # x + # x0 → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: # x + # x0

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  x = a + x3, x + x0 ≠ [], max(x + x0) ≠ max(x0 + x), ∀ x1, x2. # x1 + # x2 < # x + # x0 → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  max((a ' + x3) + x0) ≠ max(x0 + a ' + x3), ∀ x1, x2. # x1 + # x2 < #(a + x3) + # x0 → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  x3 + x0 ≠ [], (max(x3 + x0) < a ⊃ a;max(x3 + x0)) ≠ max(x0 + a ' + x3), ∀ x1, x2. # x1 + # x2 < #(a + x3) + # x0 → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

Used simplifier rules: max-base: ⊦ max(a ') = a; ⊦ x + y = [] ↔ x = [] ∧ y = []; (as) ⊦ [] + x = x; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: x3 + x0, a

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

Lemma max-rec

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 9:

  x0 = a0 + x, x3 + x0 ≠ [], (max(x3 + x0) < a ⊃ a;max(x3 + x0)) ≠ max(x0 + a ' + x3), ∀ x1, x2. # x1 + # x2 < #(a + x3) + # x0 → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

Used simplifier rules: max-rec: ⊦ x ≠ [] → max(a ' + x) = (max(x) < a ⊃ a;max(x)); list freely generated by [], +;; ⊦ x + [] = x; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  (max(x3 + a0 ' + x) < a ⊃ a;max(x3 + a0 ' + x)) ≠ max((a0 ' + x) + a ' + x3), ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

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

Proof step 10 from proof max-com (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))

• Proof step 12:

  x + a ' + x3 ≠ [], (max(x3 + a0 ' + x) < a ⊃ a;max(x3 + a0 ' + x)) ≠ (max(x + a ' + x3) < a0 ⊃ a0;max(x + a ' + x3)), ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

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

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

Lemma max-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (max(x3 + a0 ' + x) < a ⊃ a;max(x3 + a0 ' + x)) ≠ (max(x + a ' + x3) < a0 ⊃ a0;max(x + a ' + x3)), ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

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

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

User applied rule apply induction

And obtained the following new goals

• Proof step 14:

  (max(x3 + a0 ' + x) < a ⊃ a;max(x3 + a0 ' + x)) ≠ (max(x + a ' + x3) < a0 ⊃ a0;max(x + a ' + x3)), ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦ x3 + (a0 + x) ≠ [] ∧ max(x3 + (a0 + x)) ≠ max((a0 + x) + x3)

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ m +1 = m + 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m + n < m + n0 ↔ n < n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: x3, a0 + x

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  max(x3 + a0 ' + x) = max((a0 ' + x) + x3), (max((a0 ' + x) + x3) < a ⊃ a;max((a0 ' + x) + x3)) ≠ (max(x + a ' + x3) < a0 ⊃ a0;max(x + a ' + x3)), ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

• Proof step 17:

  x + x3 = [], max(x3 + a0 ' + x) = max((a0 ' + x) + x3), (max((a0 ' + x) + x3) < a ⊃ a;max((a0 ' + x) + x3)) ≠ (max(x + a ' + x3) < a0 ⊃ a0;max(x + a ' + x3)), ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

• Proof step 20:

  max(x3 + a0 ' + x) = (max(x + x3) < a0 ⊃ a0;max(x + x3)), x + x3 ≠ [], ((max(x + x3) < a0 ⊃ a0;max(x + x3)) < a ⊃ a;(max(x + x3) < a0 ⊃ a0;max(x + x3))) ≠ (max(x + a ' + x3) < a0 ⊃ a0;max(x + a ' + x3)), ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: x + x3, a0

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

Lemma max-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  (a0 < a ⊃ a;a0) ≠ (a < a0 ⊃ a0;a), ∀ x1, x2. # x1 + # x2 < #(a + []) + #(a0 + []) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

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

Proof step 18 from proof max-com (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 19:

  a0 ≠ (a < a0 ⊃ a0;a), ¬ a0 < a, ∀ x1, x2. # x1 + # x2 < #(a + []) + #(a0 + []) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a < b → (b < a ↔ false); (ss)

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

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ b < a → (a < b ↔ a ≠ b); (ss)

Proof step 20 from proof max-com (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 21:

  max(x3 + a0 ' + x) = (max(x + x3) < a0 ⊃ a0;max(x + x3)), x + x3 ≠ [], ((max(x + x3) < a0 ⊃ a0;max(x + x3)) < a ⊃ a;(max(x + x3) < a0 ⊃ a0;max(x + x3))) ≠ (max(x + a ' + x3) < a0 ⊃ a0;max(x + a ' + x3)), ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦ x + (a + x3) ≠ [] ∧ max(x + (a + x3)) ≠ max((a + x3) + x)

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ m +1 = m + 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m + n < m + n0 ↔ n < n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: x, a + x3

Proof step 21 from proof max-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  max(x3 + a0 ' + x) = (max(x + x3) < a0 ⊃ a0;max(x + x3)), max(x + a ' + x3) = max((a ' + x3) + x), x + x3 ≠ [], ((max(x + x3) < a0 ⊃ a0;max(x + x3)) < a ⊃ a;(max(x + x3) < a0 ⊃ a0;max(x + x3))) ≠ (max((a ' + x3) + x) < a0 ⊃ a0;max((a ' + x3) + x)), ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

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

Proof step 22 from proof max-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  max(x + a ' + x3) = (max(x3 + x) < a ⊃ a;max(x3 + x)), max(x3 + a0 ' + x) = (max(x + x3) < a0 ⊃ a0;max(x + x3)), x3 + x ≠ [], x + x3 ≠ [], ((max(x + x3) < a0 ⊃ a0;max(x + x3)) < a ⊃ a;(max(x + x3) < a0 ⊃ a0;max(x + x3))) ≠ ((max(x3 + x) < a ⊃ a;max(x3 + x)) < a0 ⊃ a0;(max(x3 + x) < a ⊃ a;max(x3 + x))), ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

Used simplifier rules: max-base: ⊦ max(a ') = a; ⊦ x + y = [] ↔ x = [] ∧ y = []; (as) ⊦ x + [] = x; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: x3 + x, a

Proof step 23 from proof max-com (previous step) (back to tree)

Lemma max-rec

Proof step 24 from proof max-com (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 25:

  max(x3 + a0 ' + x) = (max(x + x3) < a0 ⊃ a0;max(x + x3)), max(x + a ' + x3) = (max(x3 + x) < a ⊃ a;max(x3 + x)), x3 + x ≠ [], x + x3 ≠ [], ((max(x + x3) < a0 ⊃ a0;max(x + x3)) < a ⊃ a;(max(x + x3) < a0 ⊃ a0;max(x + x3))) ≠ ((max(x3 + x) < a ⊃ a;max(x3 + x)) < a0 ⊃ a0;(max(x3 + x) < a ⊃ a;max(x3 + x))), ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦ x + x3 ≠ [] ∧ max(x + x3) ≠ max(x3 + x)

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ m +1 = m + 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m + m0 ≤ m ↔ m0 = 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: x, x3

Proof step 25 from proof max-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  max(x + a ' + x3) = (max(x3 + x) < a ⊃ a;max(x3 + x)), max(x3 + a0 ' + x) = (max(x3 + x) < a0 ⊃ a0;max(x3 + x)), max(x + x3) = max(x3 + x), x3 + x ≠ [], x + x3 ≠ [], ((max(x3 + x) < a0 ⊃ a0;max(x3 + x)) < a ⊃ a;(max(x3 + x) < a0 ⊃ a0;max(x3 + x))) ≠ ((max(x3 + x) < a ⊃ a;max(x3 + x)) < a0 ⊃ a0;(max(x3 + x) < a ⊃ a;max(x3 + x))), ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

Proof step 26 from proof max-com (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 27:

  max(x + x3) = max(x3 + x), max(x3 + a0 ' + x) = (max(x3 + x) < a0 ⊃ a0;max(x3 + x)), max(x + a ' + x3) = (max(x3 + x) < a ⊃ a;max(x3 + x)), x3 + x ≠ [], x + x3 ≠ [], (max(x3 + x) < a0 ⊃ a0;max(x3 + x)) ≠ ((max(x3 + x) < a ⊃ a;max(x3 + x)) < a0 ⊃ a0;(max(x3 + x) < a ⊃ a;max(x3 + x))), ¬ (max(x3 + x) < a0 ⊃ a0;max(x3 + x)) < a, ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a < b → (b < a ↔ false); (ss) nnn: ⊦ ¬ c < b ∧ ¬ a < c → ¬ a < b; (forward) from specification oelem nen: ⊦ ¬ b < a ∧ a = c → ¬ b < c; (forward) from specification oelem transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification oelem lel: ⊦ a < b ∧ a = c → c < b; (forward) from specification oelem ⊦ ¬ a < a; (s)

Proof step 27 from proof max-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  max(x + x3) = max(x3 + x), max(x3 + a0 ' + x) = a0, max(x + a ' + x3) = a, x + x3 ≠ [], x3 + x ≠ [], (max(x3 + x) < a0 ⊃ a0;max(x3 + x)) ≠ ((max(x3 + x) < a ⊃ a;max(x3 + x)) < a0 ⊃ a0;(max(x3 + x) < a ⊃ a;max(x3 + x))), ¬ a0 < a, ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

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

Proof step 28 from proof max-com (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 29:

  max(x + a ' + x3) = a, max(x3 + a0 ' + x) = a0, max(x + x3) = max(x3 + x), x + x3 ≠ [], x3 + x ≠ [], a0 ≠ ((max(x3 + x) < a ⊃ a;max(x3 + x)) < a0 ⊃ a0;(max(x3 + x) < a ⊃ a;max(x3 + x))), max(x3 + x) < a0, ¬ a0 < a, ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

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

Proof step 29 from proof max-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  max(x + a ' + x3) = a, max(x3 + a0 ' + x) = a0, max(x + x3) = max(x3 + x), x3 + x ≠ [], x + x3 ≠ [], a0 ≠ ((max(x3 + x) < a ⊃ a;max(x3 + x)) < a0 ⊃ a0;a), max(x3 + x) < a0, ¬ a0 < a, ∀ x1, x2. # x1 + # x2 < #(a + x3) + #(a0 + x) → x1 + x2 ≠ [] ∧ max(x1 + x2) ≠ max(x2 + x1) → false ⊦

Rule argument

Additional information

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

Proof step 30 from proof max-com (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss) lel: ⊦ a < b ∧ a = c → c < b; (forward) from specification oelem ⊦ ¬ a < a; (s) nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification oelem nen: ⊦ ¬ b < a ∧ a = c → ¬ b < c; (forward) from specification oelem