Proof step 1 from proof notdups-map-injective (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬ dups(x) ⊦ ¬ dups(x.map(f)) ↔ (∀ a, b. a ∈ x ∧ b ∈ x ∧ a ≠ b → f(a) ≠ f(b))

Rule argument

Additional information

Proof step 2 from proof notdups-map-injective (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ dups(x) ↔ (∃ a, x0, y, z. x = x0 + (a + (y + (a + z))))

• Proof step 4:

  ∀ a, x0, y, z. x ≠ x0 + (a + (y + (a + z))) ⊦ ¬ dups(x.map(f)) ↔ (∀ a, b. a ∈ x ∧ b ∈ x ∧ a ≠ b → f(a) ≠ f(b))

Rule argument

Additional information

Used terms: x

Proof step 3 from proof notdups-map-injective (previous step) (back to tree)

Lemma dups

Proof step 4 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ∀ a, x0, y, z. x ≠ x0 + a ' + y + a ' + z ⊦ ¬ dups(x.map(f)) ↔ (∀ a, b. a ∈ x ∧ b ∈ x ∧ a ≠ b → f(a) ≠ f(b))

Rule argument

Additional information

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

Proof step 5 from proof notdups-map-injective (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ dups(x) ↔ (∃ a, x0, y, z. x = x0 + (a + (y + (a + z))))

• Proof step 7:

  ∀ a, x0, y, z. x ≠ x0 + a ' + y + a ' + z ⊦ ¬(∃ fa, bx, bx0, bx1. x.map(f) = bx + (fa + (bx0 + (fa + bx1)))) ↔ (∀ a, b. a ∈ x ∧ b ∈ x ∧ a ≠ b → f(a) ≠ f(b))

Rule argument

Additional information

Used terms: x.map(f)

Proof step 6 from proof notdups-map-injective (previous step) (back to tree)

Lemma dups

Proof step 7 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ∀ a, x0, y, z. x ≠ x0 + a ' + y + a ' + z ⊦ ¬(∃ fa, bx, bx0, bx1. x.map(f) = bx + fa ' + bx0 + fa ' + bx1) ↔ (∀ a, b. a ∈ x ∧ b ∈ x ∧ a ≠ b → f(a) ≠ f(b))

Rule argument

Additional information

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

Proof step 8 from proof notdups-map-injective (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  ∀ a, x0, y, z. x ≠ x0 + a ' + y + a ' + z ⊦ ∀ a, b. a ∈ x ∧ b ∈ x ∧ a ≠ b → f(a) ≠ f(b), ∃ fa, bx, bx0, bx1. x.map(f) = bx + fa ' + bx0 + fa ' + bx1

• Proof step 22:

  ∀ a, x0, y, z. x ≠ x0 + a ' + y + a ' + z, ∀ a, b. a ∈ x ∧ b ∈ x ∧ a ≠ b → f(a) ≠ f(b), ∃ fa, bx, bx0, bx1. x.map(f) = bx + fa ' + bx0 + fa ' + bx1 ⊦

Rule argument

Additional information

Proof step 9 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  f(a) = f(b), a ≠ b, a ∈ x, b ∈ x, ∀ a, x0, y, z. x ≠ x0 + a ' + y + a ' + z ⊦ ∃ fa, bx, bx0, bx1. x.map(f) = bx + fa ' + bx0 + fa ' + bx1

Rule argument

Additional information

Proof step 10 from proof notdups-map-injective (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ a ∈ x ↔ (∃ y, z. x = y + (a + z))

• Proof step 12:

  f(a) = f(b), a ≠ b, b ∈ x, ∀ a, x0, y, z. x ≠ x0 + a ' + y + a ' + z, ∃ y, z. x = y + (a + z) ⊦ ∃ fa, bx, bx0, bx1. x.map(f) = bx + fa ' + bx0 + fa ' + bx1

Rule argument

Additional information

Used terms: a, x

Proof step 11 from proof notdups-map-injective (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  f(a) = f(b), a ≠ b, ∀ a0, x0, y0, z0. y + a ' + z ≠ x0 + a0 ' + y0 + a0 ' + z0, b ∈ y ∨ b ∈ z ⊦ ∃ fa, bx, bx0, bx1. y.map(f) + f(b) ' + z.map(f) = bx + fa ' + bx0 + fa ' + bx1

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).map(f) = f(a) + x.map(f); (s) ⊦ (x + y).map(f) = x.map(f) + y.map(f); (s) ⊦ a ≠ a0 → (a ∈ a0 ' + x ↔ a ∈ x); (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s)

Proof step 13 from proof notdups-map-injective (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  f(a) = f(b), a ≠ b, b ∈ y, ∀ a0, x0, y0, z0. y + a ' + z ≠ x0 + a0 ' + y0 + a0 ' + z0 ⊦ ∃ fa, bx, bx0, bx1. y.map(f) + f(b) ' + z.map(f) = bx + fa ' + bx0 + fa ' + bx1

• Proof step 18:

  f(a) = f(b), a ≠ b, b ∈ z, ∀ a0, x0, y0, z0. y + a ' + z ≠ x0 + a0 ' + y0 + a0 ' + z0 ⊦ ∃ fa, bx, bx0, bx1. y.map(f) + f(b) ' + z.map(f) = bx + fa ' + bx0 + fa ' + bx1

Rule argument

Additional information

Proof step 14 from proof notdups-map-injective (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ a ∈ x ↔ (∃ y, z. x = y + (a + z))

• Proof step 16:

  f(a) = f(b), a ≠ b, ∀ a0, x0, y0, z0. y + a ' + z ≠ x0 + a0 ' + y0 + a0 ' + z0, ∃ y0, z. y = y0 + (b + z) ⊦ ∃ fa, bx, bx0, bx1. y.map(f) + f(b) ' + z.map(f) = bx + fa ' + bx0 + fa ' + bx1

Rule argument

Additional information

Used terms: b, y

Proof step 15 from proof notdups-map-injective (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  f(a) = f(b), a ≠ b, ∀ a0, x0, y1, z1. y0 + (b ' + z0) + a ' + z ≠ x0 + a0 ' + y1 + a0 ' + z1 ⊦ ∃ fa, bx, bx0, bx1. (y0.map(f) + f(b) ' + z0.map(f)) + f(b) ' + z.map(f) = bx + fa ' + bx0 + fa ' + bx1

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).map(f) = f(a) + x.map(f); (s) ⊦ (x + y).map(f) = x.map(f) + y.map(f); (s)

Proof step 17 from proof notdups-map-injective (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; from specification list Used terms: f(b), y0.map(f), z0.map(f), z.map(f)

Proof step 18 from proof notdups-map-injective (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ a ∈ x ↔ (∃ y, z. x = y + (a + z))

• Proof step 20:

  f(a) = f(b), a ≠ b, ∀ a0, x0, y0, z0. y + a ' + z ≠ x0 + a0 ' + y0 + a0 ' + z0, ∃ y, z0. z = y + (b + z0) ⊦ ∃ fa, bx, bx0, bx1. y.map(f) + f(b) ' + z.map(f) = bx + fa ' + bx0 + fa ' + bx1

Rule argument

Additional information

Used terms: b, z

Proof step 19 from proof notdups-map-injective (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  f(a) = f(b), a ≠ b, ∀ a0, x0, y1, z1. y + a ' + y0 + b ' + z0 ≠ x0 + a0 ' + y1 + a0 ' + z1 ⊦ ∃ fa, bx, bx0, bx1. y.map(f) + f(b) ' + y0.map(f) + f(b) ' + z0.map(f) = bx + fa ' + bx0 + fa ' + bx1

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).map(f) = f(a) + x.map(f); (s) ⊦ (x + y).map(f) = x.map(f) + y.map(f); (s)

Proof step 21 from proof notdups-map-injective (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; from specification list Used terms: f(b), y.map(f), y0.map(f), z0.map(f)

Proof step 22 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  x.map(f) = bx + fa ' + bx0 + fa ' + bx1, ∀ a, b. a ∈ x ∧ b ∈ x ∧ a ≠ b → f(a) ≠ f(b), ∀ a, x0, y, z. x ≠ x0 + a ' + y + a ' + z ⊦

Rule argument

Additional information

Proof step 23 from proof notdups-map-injective (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 24:

  (a + x0).map(f) = bx + fa ' + bx0 + fa ' + bx1, ∀ a0, x1, y, z. a + x0 ≠ x1 + a0 ' + y + a0 ' + z, ∀ a0, b. a0 ∈ a + x0 ∧ b ∈ a + x0 ∧ a0 ≠ b → f(a0) ≠ f(b), ∀ f, bx, fa, bx0, bx1. ¬(x0.map(f) = bx + fa ' + bx0 + fa ' + bx1 ∧ (∀ a, b. a ∈ x0 ∧ b ∈ x0 ∧ a ≠ b → f(a) ≠ f(b)) ∧ (∀ a, x1, y, z. x0 ≠ x1 + a ' + y + a ' + z)) ⊦

Rule argument

Additional information

Used simplifier rules: List[A] freely generated by [], +; ⊦ [].map(f) = []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 24 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  f(a) ' + x0.map(f) = bx + fa ' + bx0 + fa ' + bx1, ∀ a0, x1, y, z. a ' + x0 ≠ x1 + a0 ' + y + a0 ' + z, ∀ a0, b. (a0 = a ∨ a0 ∈ x0) ∧ (b = a ∨ b ∈ x0) ∧ a0 ≠ b → f(a0) ≠ f(b), ∀ f0, bx2, fa0, bx3, bx4. x0.map(f0) ≠ bx2 + fa0 ' + bx3 + fa0 ' + bx4 ∨ ¬(∀ a, b. a ∈ x0 ∧ b ∈ x0 ∧ a ≠ b → f0(a) ≠ f0(b)) ∨ ¬(∀ a, x1, y, z. x0 ≠ x1 + a ' + y + a ' + z), f(a) ∈ bx ∨ f(a) = fa ∨ f(a) ∈ bx0 ∨ f(a) ∈ bx1 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ≠ a0 → (a ∈ a0 ' + x ↔ a ∈ x); (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).map(f) = f(a) + x.map(f); (s)

Proof step 25 from proof notdups-map-injective (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 26:

  f(a) ' + x0.map(f) = bx + fa ' + bx0 + fa ' + bx1, bx = [], ∀ f0, bx2, fa0, bx3, bx4. x0.map(f0) ≠ bx2 + fa0 ' + bx3 + fa0 ' + bx4 ∨ ¬(∀ a, b. a ∈ x0 ∧ b ∈ x0 ∧ a ≠ b → f0(a) ≠ f0(b)) ∨ ¬(∀ a, x1, y, z. x0 ≠ x1 + a ' + y + a ' + z), ∀ a0, b. (a0 = a ∨ a0 ∈ x0) ∧ (b = a ∨ b ∈ x0) ∧ a0 ≠ b → f(a0) ≠ f(b), ∀ a0, x1, y, z. a ' + x0 ≠ x1 + a0 ' + y + a0 ' + z, f(a) ∈ bx ∨ f(a) = fa ∨ f(a) ∈ bx0 ∨ f(a) ∈ bx1 ⊦

• Proof step 35:

  f(a) ' + x0.map(f) = bx + fa ' + bx0 + fa ' + bx1, bx = fa1 + bx5, ∀ f0, bx2, fa0, bx3, bx4. x0.map(f0) ≠ bx2 + fa0 ' + bx3 + fa0 ' + bx4 ∨ ¬(∀ a, b. a ∈ x0 ∧ b ∈ x0 ∧ a ≠ b → f0(a) ≠ f0(b)) ∨ ¬(∀ a, x1, y, z. x0 ≠ x1 + a ' + y + a ' + z), ∀ a0, b. (a0 = a ∨ a0 ∈ x0) ∧ (b = a ∨ b ∈ x0) ∧ a0 ≠ b → f(a0) ≠ f(b), ∀ a0, x1, y, z. a ' + x0 ≠ x1 + a0 ' + y + a0 ' + z, f(a) ∈ bx ∨ f(a) = fa ∨ f(a) ∈ bx0 ∨ f(a) ∈ bx1 ⊦

Rule argument

Additional information

Used simplifier rules: List[A] freely generated by [], +;

Proof step 26 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  x0.map(f) = bx0 + f(a) ' + bx1, ∀ f0, bx2, fa0, bx3, bx4. x0.map(f0) ≠ bx2 + fa0 ' + bx3 + fa0 ' + bx4 ∨ ¬(∀ a, b. a ∈ x0 ∧ b ∈ x0 ∧ a ≠ b → f0(a) ≠ f0(b)) ∨ ¬(∀ a, x1, y, z. x0 ≠ x1 + a ' + y + a ' + z), ∀ a0, b. (a0 = a ∨ a0 ∈ x0) ∧ (b = a ∨ b ∈ x0) ∧ a0 ≠ b → f(a0) ≠ f(b), ∀ a0, x1, y, z. a ' + x0 ≠ x1 + a0 ' + y + a0 ' + z ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws) ⊦ [] + x = x; (s)

Proof step 27 from proof notdups-map-injective (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 28:

  x0.map(f) = bx0 + f(a) ' + bx1, f(a) ∈ x0.map(f), ∀ a0, x1, y, z. a ' + x0 ≠ x1 + a0 ' + y + a0 ' + z, ∀ a0, b. (a0 = a ∨ a0 ∈ x0) ∧ (b = a ∨ b ∈ x0) ∧ a0 ≠ b → f(a0) ≠ f(b), ∀ f0, bx2, fa0, bx3, bx4. x0.map(f0) ≠ bx2 + fa0 ' + bx3 + fa0 ' + bx4 ∨ ¬(∀ a, b. a ∈ x0 ∧ b ∈ x0 ∧ a ≠ b → f0(a) ≠ f0(b)) ∨ ¬(∀ a, x1, y, z. x0 ≠ x1 + a ' + y + a ' + z) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ x → x ≠ y + a ' + z; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used formulas: f(a) ∈ x0.map(f)

Proof step 28 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  x0.map(f) = bx0 + f(a0) ' + bx1, f(a) = f(a0), a0 ∈ x0, ∀ f0, bx2, fa0, bx3, bx4. x0.map(f0) ≠ bx2 + fa0 ' + bx3 + fa0 ' + bx4 ∨ ¬(∀ a, b. a ∈ x0 ∧ b ∈ x0 ∧ a ≠ b → f0(a) ≠ f0(b)) ∨ ¬(∀ a, x1, y, z. x0 ≠ x1 + a ' + y + a ' + z), ∀ a0, b. (a0 = a ∨ a0 ∈ x0) ∧ (b = a ∨ b ∈ x0) ∧ a0 ≠ b → f(a0) ≠ f(b), ∀ a0, x1, y, z. a ' + x0 ≠ x1 + a0 ' + y + a0 ' + z ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ b ∈ x.map(f) ↔ (∃ a. b = f(a) ∧ a ∈ x); (as)

Proof step 29 from proof notdups-map-injective (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ a ∈ x ↔ (∃ y, z. x = y + (a + z))

• Proof step 31:

  x0.map(f) = bx0 + f(a0) ' + bx1, f(a) = f(a0), ∀ a0, x1, y, z. a ' + x0 ≠ x1 + a0 ' + y + a0 ' + z, ∀ a0, b. (a0 = a ∨ a0 ∈ x0) ∧ (b = a ∨ b ∈ x0) ∧ a0 ≠ b → f(a0) ≠ f(b), ∀ f0, bx2, fa0, bx3, bx4. x0.map(f0) ≠ bx2 + fa0 ' + bx3 + fa0 ' + bx4 ∨ ¬(∀ a, b. a ∈ x0 ∧ b ∈ x0 ∧ a ≠ b → f0(a) ≠ f0(b)) ∨ ¬(∀ a, x1, y, z. x0 ≠ x1 + a ' + y + a ' + z), ∃ y, z. x0 = y + (a0 + z) ⊦

Rule argument

Additional information

Used terms: a0, x0

Proof step 30 from proof notdups-map-injective (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  y.map(f) + f(a0) ' + z.map(f) = bx0 + f(a0) ' + bx1, f(a) = f(a0), ∀ f0, bx2, fa0, bx3, bx4. y.map(f0) + f0(a0) ' + z.map(f0) ≠ bx2 + fa0 ' + bx3 + fa0 ' + bx4 ∨ ¬(∀ a1, b. (a1 ∈ y ∨ a1 = a0 ∨ a1 ∈ z) ∧ (b ∈ y ∨ b = a0 ∨ b ∈ z) ∧ a1 ≠ b → f0(a1) ≠ f0(b)) ∨ ¬(∀ a1, x1, y0, z0. y + a0 ' + z ≠ x1 + a1 ' + y0 + a1 ' + z0), ∀ a1, b. (a1 = a ∨ a1 ∈ y ∨ a1 = a0 ∨ a1 ∈ z) ∧ (b = a ∨ b ∈ y ∨ b = a0 ∨ b ∈ z) ∧ a1 ≠ b → f(a1) ≠ f(b), ∀ a1, x1, y0, z0. a ' + y + a0 ' + z ≠ x1 + a1 ' + y0 + a1 ' + z0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ (a ' + x).map(f) = f(a) + x.map(f); (s) ⊦ (x + y).map(f) = x.map(f) + y.map(f); (s)

Proof step 32 from proof notdups-map-injective (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 33:

  y.map(f) + f(a0) ' + z.map(f) = bx0 + f(a0) ' + bx1, f(a) = f(a0), (a = a ∨ a ∈ y ∨ a = a0 ∨ a ∈ z) ∧ (a0 = a ∨ a0 ∈ y ∨ a0 = a0 ∨ a0 ∈ z) ∧ a ≠ a0 → f(a) ≠ f(a0), ∀ a1, x1, y0, z0. a ' + y + a0 ' + z ≠ x1 + a1 ' + y0 + a1 ' + z0, ∀ a1, b. (a1 = a ∨ a1 ∈ y ∨ a1 = a0 ∨ a1 ∈ z) ∧ (b = a ∨ b ∈ y ∨ b = a0 ∨ b ∈ z) ∧ a1 ≠ b → f(a1) ≠ f(b), ∀ f0, bx2, fa0, bx3, bx4. y.map(f0) + f0(a0) ' + z.map(f0) ≠ bx2 + fa0 ' + bx3 + fa0 ' + bx4 ∨ ¬(∀ a1, b. (a1 ∈ y ∨ a1 = a0 ∨ a1 ∈ z) ∧ (b ∈ y ∨ b = a0 ∨ b ∈ z) ∧ a1 ≠ b → f0(a1) ≠ f0(b)) ∨ ¬(∀ a1, x1, y0, z0. y + a0 ' + z ≠ x1 + a1 ' + y0 + a1 ' + z0) ⊦

Rule argument

Additional information

Used terms: a, a0

Proof step 33 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  y.map(f) + f(a0) ' + z.map(f) = bx0 + f(a0) ' + bx1, ∀ a1, b. (a1 ∈ y ∨ a1 = a0 ∨ a1 ∈ z) ∧ (b ∈ y ∨ b = a0 ∨ b ∈ z) ∧ a1 ≠ b → f(a1) ≠ f(b), ∀ a1, x1, y0, z0. a0 ' + y + a0 ' + z ≠ x1 + a1 ' + y0 + a1 ' + z0, ∀ f0, bx2, fa0, bx3, bx4. y.map(f0) + f0(a0) ' + z.map(f0) ≠ bx2 + fa0 ' + bx3 + fa0 ' + bx4 ∨ ¬(∀ a1, b. (a1 ∈ y ∨ a1 = a0 ∨ a1 ∈ z) ∧ (b ∈ y ∨ b = a0 ∨ b ∈ z) ∧ a1 ≠ b → f0(a1) ≠ f0(b)) ∨ ¬(∀ a1, x1, y0, z0. y + a0 ' + z ≠ x1 + a1 ' + y0 + a1 ' + z0) ⊦

Rule argument

Additional information

Proof step 34 from proof notdups-map-injective (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ [] + x = x; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: a0, [], y, z

Proof step 35 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  x0.map(f) = bx5 + fa ' + bx0 + fa ' + bx1, ∀ f0, bx2, fa0, bx3, bx4. x0.map(f0) ≠ bx2 + fa0 ' + bx3 + fa0 ' + bx4 ∨ ¬(∀ a, b. a ∈ x0 ∧ b ∈ x0 ∧ a ≠ b → f0(a) ≠ f0(b)) ∨ ¬(∀ a, x1, y, z. x0 ≠ x1 + a ' + y + a ' + z), ∀ a0, b. (a0 = a ∨ a0 ∈ x0) ∧ (b = a ∨ b ∈ x0) ∧ a0 ≠ b → f(a0) ≠ f(b), ∀ a0, x1, y, z. a ' + x0 ≠ x1 + a0 ' + y + a0 ' + z ⊦

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 + x = a ' + x; (s) ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws)

Proof step 36 from proof notdups-map-injective (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 37:

  x0.map(f) = bx5 + fa ' + bx0 + fa ' + bx1, ∀ a0, x1, y, z. a ' + x0 ≠ x1 + a0 ' + y + a0 ' + z, ∀ a0, b. (a0 = a ∨ a0 ∈ x0) ∧ (b = a ∨ b ∈ x0) ∧ a0 ≠ b → f(a0) ≠ f(b), x0.map(f) ≠ bx5 + fa ' + bx0 + fa ' + bx1 ∨ ¬(∀ a, b. a ∈ x0 ∧ b ∈ x0 ∧ a ≠ b → f(a) ≠ f(b)) ∨ ¬(∀ a, x1, y, z. x0 ≠ x1 + a ' + y + a ' + z) ⊦

Rule argument

Additional information

Used terms: f, bx5, fa, bx0, bx1

Proof step 37 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  x0.map(f) = bx5 + fa ' + bx0 + fa ' + bx1, ∀ a0, b. (a0 = a ∨ a0 ∈ x0) ∧ (b = a ∨ b ∈ x0) ∧ a0 ≠ b → f(a0) ≠ f(b), ∀ a0, x1, y, z. a ' + x0 ≠ x1 + a0 ' + y + a0 ' + z, ¬(a0 ∈ x0 ∧ b ∈ x0 ∧ a0 ≠ b → f(a0) ≠ f(b)) ∨ x0 = x1 + a1 ' + y + a1 ' + z ⊦

Rule argument

Additional information

Proof step 38 from proof notdups-map-injective (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 39:

  x0.map(f) = bx5 + fa ' + bx0 + fa ' + bx1, f(a0) = f(b), a0 ≠ b, a0 ∈ x0, b ∈ x0, ∀ a0, x1, y, z. a ' + x0 ≠ x1 + a0 ' + y + a0 ' + z, ∀ a0, b. (a0 = a ∨ a0 ∈ x0) ∧ (b = a ∨ b ∈ x0) ∧ a0 ≠ b → f(a0) ≠ f(b) ⊦

• Proof step 40:

  x0.map(f) = bx5 + fa ' + bx0 + fa ' + bx1, x0 = x1 + a1 ' + y + a1 ' + z, ∀ a0, x1, y, z. a ' + x0 ≠ x1 + a0 ' + y + a0 ' + z, ∀ a0, b. (a0 = a ∨ a0 ∈ x0) ∧ (b = a ∨ b ∈ x0) ∧ a0 ≠ b → f(a0) ≠ f(b) ⊦

Rule argument

Additional information

Proof step 39 from proof notdups-map-injective (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a0, b

Proof step 40 from proof notdups-map-injective (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  x1.map(f) + f(a1) ' + y.map(f) + f(a1) ' + z.map(f) = bx5 + fa ' + bx0 + fa ' + bx1, ∀ a0, x, y0, z0. a ' + x1 + a1 ' + y + a1 ' + z ≠ x + a0 ' + y0 + a0 ' + z0, ∀ a0, b. (a0 = a ∨ a0 ∈ x1 ∨ a0 = a1 ∨ a0 ∈ y ∨ a0 ∈ z) ∧ (b = a ∨ b ∈ x1 ∨ b = a1 ∨ b ∈ y ∨ b ∈ z) ∧ a0 ≠ b → f(a0) ≠ f(b) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ≠ a0 → (a ∈ a0 ' + x ↔ a ∈ x); (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).map(f) = f(a) + x.map(f); (s) ⊦ (x + y).map(f) = x.map(f) + y.map(f); (s)

Proof step 41 from proof notdups-map-injective (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 Used terms: a1, a ' + x1, y, z