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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

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

User applied rule induction

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  min((a ' + x3) + x0) ≠ min(x0 + a ' + x3), ∀ x1, x2. #(x1 + x2) < #((a + x3) + x0) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 7 from proof min-com (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  x3 + a0 ' + x ≠ [], (a < min(x3 + a0 ' + x) ⊃ a;min(x3 + a0 ' + x)) ≠ min((a0 ' + x) + a ' + x3), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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: x3 + a0 ' + x, a

Proof step 10 from proof min-com (previous step) (back to tree)

Lemma min-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  (a < min(x3 + a0 ' + x) ⊃ a;min(x3 + a0 ' + x)) ≠ min((a0 ' + x) + a ' + x3), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 12 from proof min-com (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 13:

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

• Proof step 54:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  x + a ' + x3 ≠ [], a ≠ (a0 < min(x + a ' + x3) ⊃ a0;min(x + a ' + x3)), a < min(x3 + a0 ' + x), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 14 from proof min-com (previous step) (back to tree)

Lemma min-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  a ≠ (a0 < min(x + a ' + x3) ⊃ a0;min(x + a ' + x3)), a < min(x3 + a0 ' + x), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 16 from proof min-com (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 17:

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

• Proof step 31:

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

Rule argument

Additional information

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

User applied rule apply induction

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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 18 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  min(x + a ' + x3) = min((a ' + x3) + x), a ≠ a0, a < min(x3 + a0 ' + x), a0 < min((a ' + x3) + x), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 19 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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 20 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  min(x + a ' + x3) = min((a ' + x3) + x), min(x3 + a0 ' + x) = min((a0 ' + x) + x3), a ≠ a0, a < min((a0 ' + x) + x3), a0 < min((a ' + x3) + x), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 21 from proof min-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

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

• Proof step 23:

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

Rule argument

Additional information

Used simplifier rules: min-base: ⊦ min(a ') = a; ⊦ x + y = [] ↔ x = [] ∧ y = []; (as) ⊦ [] + x = x; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ ¬ a < a; (s) Used terms: x + x3, a0

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

Lemma min-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

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

Rule argument

Additional information

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 25:

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

• Proof step 28:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord]

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

Used simplifier rules: min-base: ⊦ min(a ') = a; transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ ¬ a < a; (s) ⊦ 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 27 from proof min-com (previous step) (back to tree)

Lemma min-rec

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

Used simplifier rules: min-base: ⊦ min(a ') = a; ⊦ ¬ a < a; (s) transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ 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 30 from proof min-com (previous step) (back to tree)

Lemma min-rec

Proof step 31 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

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

Rule argument

Additional information

Proof step 32 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 33:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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 33 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  min(x + a ' + x3) = min((a ' + x3) + x), a ≠ min((a ' + x3) + x), a < min(x3 + a0 ' + x), ¬ a0 < min((a ' + x3) + x), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 34 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 35:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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 35 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  min(x + a ' + x3) = min((a ' + x3) + x), min(x3 + a0 ' + x) = min((a0 ' + x) + x3), a ≠ min((a ' + x3) + x), a < min((a0 ' + x) + x3), ¬ a0 < min((a ' + x3) + x), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 36 from proof min-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

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

• Proof step 38:

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

Rule argument

Additional information

Used simplifier rules: min-base: ⊦ min(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: x + x3, a0

Proof step 37 from proof min-com (previous step) (back to tree)

Lemma min-rec

Proof step 38 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

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

Rule argument

Additional information

Proof step 39 from proof min-com (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 40:

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

• Proof step 47:

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

Rule argument

Additional information

Proof step 40 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

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

Rule argument

Additional information

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

Proof step 41 from proof min-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

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

• Proof step 43:

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

Rule argument

Additional information

Used simplifier rules: min-base: ⊦ min(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 42 from proof min-com (previous step) (back to tree)

Lemma min-rec

Proof step 43 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

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

Rule argument

Additional information

Used simplifier rules: nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification weakord[tord]

Proof step 44 from proof min-com (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 45:

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

Rule argument

Additional information

Proof step 45 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a < b → (b < a ↔ false); (ss) transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss)

Proof step 46 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ ¬ a < a; (s) ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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: x3, x

Proof step 47 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

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

Rule argument

Additional information

Proof step 48 from proof min-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

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

• Proof step 50:

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

Rule argument

Additional information

Used simplifier rules: min-base: ⊦ min(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 49 from proof min-com (previous step) (back to tree)

Lemma min-rec

Proof step 50 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

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

Rule argument

Additional information

Proof step 51 from proof min-com (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 52:

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

Rule argument

Additional information

Proof step 52 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

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

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss)

Proof step 53 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ ¬ a < a; (s) ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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: x3, x

Proof step 54 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

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

Rule argument

Additional information

Proof step 55 from proof min-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

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

• Proof step 57:

  x + a ' + x3 ≠ [], min(x3 + a0 ' + x) ≠ (a0 < min(x + a ' + x3) ⊃ a0;min(x + a ' + x3)), ¬ a < min(x3 + a0 ' + x), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 56 from proof min-com (previous step) (back to tree)

Lemma min-rec

Proof step 57 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  min(x3 + a0 ' + x) ≠ (a0 < min(x + a ' + x3) ⊃ a0;min(x + a ' + x3)), ¬ a < min(x3 + a0 ' + x), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 58 from proof min-com (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 59:

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

• Proof step 76:

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

Rule argument

Additional information

Proof step 59 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 60:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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 60 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  min(x + a ' + x3) = min((a ' + x3) + x), min(x3 + a0 ' + x) ≠ a0, a0 < min((a ' + x3) + x), ¬ a < min(x3 + a0 ' + x), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 61 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 62:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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 62 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  min(x + a ' + x3) = min((a ' + x3) + x), min(x3 + a0 ' + x) = min((a0 ' + x) + x3), min((a0 ' + x) + x3) ≠ a0, a0 < min((a ' + x3) + x), ¬ a < min((a0 ' + x) + x3), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 63 from proof min-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 64:

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

• Proof step 65:

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

Rule argument

Additional information

Used simplifier rules: min-base: ⊦ min(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: x + x3, a0

Proof step 64 from proof min-com (previous step) (back to tree)

Lemma min-rec

Proof step 65 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

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

Rule argument

Additional information

Proof step 66 from proof min-com (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 67:

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

Rule argument

Additional information

Proof step 67 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

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

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss)

Proof step 68 from proof min-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

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

• Proof step 70:

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

Rule argument

Additional information

Used simplifier rules: min-base: ⊦ min(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 69 from proof min-com (previous step) (back to tree)

Lemma min-rec

Proof step 70 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

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

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord]

Proof step 71 from proof min-com (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 72:

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

• Proof step 74:

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

Rule argument

Additional information

Proof step 72 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 73:

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

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ a < b → (b < a ↔ false); (ss)

Proof step 73 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ ¬ a < a; (s) ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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 74 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 75:

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

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord]

Proof step 75 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ ¬ a < a; (s) ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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 76 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 77:

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

Rule argument

Additional information

Proof step 77 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 78:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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 78 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 79:

  min(x + a ' + x3) = min((a ' + x3) + x), min(x3 + a0 ' + x) ≠ min((a ' + x3) + x), ¬ a0 < min((a ' + x3) + x), ¬ a < min(x3 + a0 ' + x), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 79 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 80:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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 80 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 81:

  min(x + a ' + x3) = min((a ' + x3) + x), min(x3 + a0 ' + x) = min((a0 ' + x) + x3), min((a0 ' + x) + x3) ≠ min((a ' + x3) + x), ¬ a0 < min((a ' + x3) + x), ¬ a < min((a0 ' + x) + x3), ∀ x1, x2. #(x1 + x2) < #((a + x3) + (a0 + x)) → x1 + x2 ≠ [] ∧ min(x1 + x2) ≠ min(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 81 from proof min-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 82:

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

• Proof step 83:

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

Rule argument

Additional information

Used simplifier rules: min-base: ⊦ min(a ') = a; ⊦ x + y = [] ↔ x = [] ∧ y = []; (as) ⊦ [] + x = x; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss) transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ ¬ a < a; (s) Used terms: x + x3, a0

Proof step 82 from proof min-com (previous step) (back to tree)

Lemma min-rec

Proof step 83 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 84:

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

Rule argument

Additional information

Proof step 84 from proof min-com (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 85:

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

• Proof step 92:

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

Rule argument

Additional information

Proof step 85 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 86:

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

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss)

Proof step 86 from proof min-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 87:

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

• Proof step 88:

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

Rule argument

Additional information

Used simplifier rules: min-base: ⊦ min(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 87 from proof min-com (previous step) (back to tree)

Lemma min-rec

Proof step 88 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 89:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a < a; (s) nll: ⊦ ¬ b < a ∧ b < c → a < c; (forward) from specification weakord[tord] transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss)

Proof step 89 from proof min-com (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 90:

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

Rule argument

Additional information

Proof step 90 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 91:

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

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord]

Proof step 91 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ ¬ a < a; (s) ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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: x3, x

Proof step 92 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 93:

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

Rule argument

Additional information

Proof step 93 from proof min-com (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 94:

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

• Proof step 95:

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

Rule argument

Additional information

Used simplifier rules: min-base: ⊦ min(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 94 from proof min-com (previous step) (back to tree)

Lemma min-rec

Proof step 95 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 96:

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

Rule argument

Additional information

Proof step 96 from proof min-com (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 97:

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

• Proof step 99:

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

Rule argument

Additional information

Proof step 97 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 98:

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

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ a ≠ b → (a < b ↔ ¬ b < a); (ss)

Proof step 98 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification weakord[tord] ⊦ ¬ a < a; (s) ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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 99 from proof min-com (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 100:

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

Rule argument

Additional information

Proof step 100 from proof min-com (previous step) (back to tree)

User applied rule apply induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +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