Proof step 1 from proof unequal (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  # x = # y, x ≠ y ⊦ ∃ z, a, b, z0, z1. a ≠ b ∧ x = z + a ' + z0 ∧ y = z + b ' + z1

Rule argument

Additional information

Proof step 2 from proof unequal (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  # x = #(a + y0), x ≠ a + y0, ∀ x. # x = # y0 ∧ x ≠ y0 → (∃ z, a, b, z0, z1. a ≠ b ∧ x = z + a ' + z0 ∧ y0 = z + b ' + z1) ⊦ ∃ z, a0, b, z0, z1. a0 ≠ b ∧ x = z + a0 ' + z0 ∧ a + y0 = z + b ' + z1

Rule argument

Additional information

Used simplifier rules: list freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ # x = 0 ↔ x = []; (s)

Proof step 3 from proof unequal (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  # x = # y0 + 1, x ≠ a ' + y0, ∀ x. # x = # y0 ∧ x ≠ y0 → (∃ z, a, b, z0, z1. a ≠ b ∧ x = z + a ' + z0 ∧ y0 = z + b ' + z1) ⊦ ∃ z, a0, b, z0, z1. a0 ≠ b ∧ x = z + a0 ' + z0 ∧ a ' + y0 = z + b ' + z1

Rule argument

Additional information

Used simplifier rules: len-05: ⊦ #(a ' + x) = (# x)+1; a: ⊦ (x + y) + z = x + y + z; c: ⊦ a + x = a ' + x; ⊦ m +1 = m + 1; (s)

Proof step 4 from proof unequal (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  # x = # y0 + 1, x = a1 + x0, x ≠ a ' + y0, ∀ x. # x = # y0 ∧ x ≠ y0 → (∃ z, a, b, z0, z1. a ≠ b ∧ x = z + a ' + z0 ∧ y0 = z + b ' + z1) ⊦ ∃ z, a0, b, z0, z1. a0 ≠ b ∧ x = z + a0 ' + z0 ∧ a ' + y0 = z + b ' + z1

Rule argument

Additional information

Used simplifier rules: list freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ m + 1 ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 5 from proof unequal (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  # x0 = # y0, a1 ' + x0 ≠ a ' + y0, ∀ x. # x = # y0 ∧ x ≠ y0 → (∃ z, a, b, z0, z1. a ≠ b ∧ x = z + a ' + z0 ∧ y0 = z + b ' + z1) ⊦ ∃ z, a0, b, z0, z1. a0 ≠ b ∧ a1 ' + x0 = z + a0 ' + z0 ∧ a ' + y0 = z + b ' + z1

Rule argument

Additional information

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

Proof step 6 from proof unequal (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 7:

  # x0 = # y0, a ' ≠ [], a1 ' + x0 ≠ a ' + y0, ∀ x. # x = # y0 ∧ x ≠ y0 → (∃ z, a, b, z0, z1. a ≠ b ∧ x = z + a ' + z0 ∧ y0 = z + b ' + z1) ⊦ ∃ z, a0, b, z0, z1. a0 ≠ b ∧ a1 ' + x0 = z + a0 ' + z0 ∧ a ' + y0 = z + b ' + z1

Rule argument

Additional information

Used simplifier rules: e: ⊦ a ' ≠ []; Used formulas: a ' = []

Proof step 7 from proof unequal (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  # x0 = # y0, a1 ' + x0 ≠ a ' + y0, ∀ x. # x = # y0 ∧ x ≠ y0 → (∃ z, a, b, z0, z1. a ≠ b ∧ x = z + a ' + z0 ∧ y0 = z + b ' + z1) ⊦ ∃ z, a0, b, z0, z1. a0 ≠ b ∧ a1 ' + x0 = z + a0 ' + z0 ∧ a ' + y0 = z + b ' + z1

Rule argument

Additional information

Used simplifier rules: e: ⊦ a ' ≠ [];

Proof step 8 from proof unequal (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 9:

  # x0 = # y0, a1 = a, a1 ' + x0 ≠ a ' + y0, ∀ x. # x = # y0 ∧ x ≠ y0 → (∃ z, a, b, z0, z1. a ≠ b ∧ x = z + a ' + z0 ∧ y0 = z + b ' + z1) ⊦ ∃ z, a0, b, z0, z1. a0 ≠ b ∧ a1 ' + x0 = z + a0 ' + z0 ∧ a ' + y0 = z + b ' + z1

• Proof step 13:

  # x0 = # y0, a1 ' + x0 ≠ a ' + y0, a1 ≠ a, ∀ x. # x = # y0 ∧ x ≠ y0 → (∃ z, a, b, z0, z1. a ≠ b ∧ x = z + a ' + z0 ∧ y0 = z + b ' + z1) ⊦ ∃ z, a0, b, z0, z1. a0 ≠ b ∧ a1 ' + x0 = z + a0 ' + z0 ∧ a ' + y0 = z + b ' + z1

Rule argument

Additional information

Used formulas: a1 = a

Proof step 9 from proof unequal (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  # x0 = # y0, x0 ≠ y0, ∀ x. # x = # y0 ∧ x ≠ y0 → (∃ z, a, b, z0, z1. a ≠ b ∧ x = z + a ' + z0 ∧ y0 = z + b ' + z1) ⊦ ∃ z, a0, b, z0, z1. a0 ≠ b ∧ a ' + x0 = z + a0 ' + z0 ∧ a ' + y0 = z + b ' + z1

Rule argument

Additional information

Used simplifier rules: app-08: ⊦ a ' + x = a ' + y ↔ x = y; a: ⊦ (x + y) + z = x + y + z;

Proof step 10 from proof unequal (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  # x0 = # y0, x0 ≠ y0, # x0 = # y0 ∧ x0 ≠ y0 → (∃ z, a, b, z0, z1. a ≠ b ∧ x0 = z + a ' + z0 ∧ y0 = z + b ' + z1), ∀ x. # x = # y0 ∧ x ≠ y0 → (∃ z, a, b, z0, z1. a ≠ b ∧ x = z + a ' + z0 ∧ y0 = z + b ' + z1) ⊦ ∃ z, a0, b, z0, z1. a0 ≠ b ∧ a ' + x0 = z + a0 ' + z0 ∧ a ' + y0 = z + b ' + z1

Rule argument

Additional information

Used terms: x0

Proof step 11 from proof unequal (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  # a0 ' + # z0 = # b ' + # z1, a0 ' + z0 ≠ b ' + z1, a0 ≠ b, ∀ x. # x = # z + # b ' + # z1 ∧ x ≠ z + b ' + z1 → (∃ z0, a, b0, z2, z3. a ≠ b0 ∧ x = z0 + a ' + z2 ∧ z + b ' + z1 = z0 + b0 ' + z3) ⊦ ∃ z2, a1, b0, z3, z4. a1 ≠ b0 ∧ a ' + z + a0 ' + z0 = z2 + a1 ' + z3 ∧ a ' + z + b ' + z1 = z2 + b0 ' + z4

Rule argument

Additional information

Used simplifier rules: app-01: ⊦ x + y = x + z ↔ y = z; len: ⊦ #(x + y) = # x + # y; a: ⊦ (x + y) + z = x + y + z; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 12 from proof unequal (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; Used terms: a ' + z, a0, b, z0, z1

Proof step 13 from proof unequal (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Nil: ⊦ [] + x = x; app-07: ⊦ a ' + x = b ' + x ↔ a = b; a: ⊦ (x + y) + z = x + y + z; Used terms: [], a1, a, x0, y0