Proof step 1 from proof in-09 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  x + a ' = y + b ' + z, b ∈ z, ¬ dups(x + a ') ⊦

Rule argument

Additional information

Proof step 2 from proof in-09 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  x + a ' = y + b ' + z, b ∈ z, ¬ dups(x), ¬ a ∈ x, a ∈ y ∨ a ∈ z, b ∈ x ∨ b = a ⊦

Rule argument

Additional information

Used simplifier rules: f: ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ b ' ↔ a = b; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) in-13: ⊦ x = y + a ' + z → a ∈ x; (forward) from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list

Proof step 3 from proof in-09 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ x ≠ [] → (∃ y, a. x = y + a ')

Rule argument

Additional information

Used simplifier rules: in-01-02: ⊦ a ∈ y → dups(x + a ' + y); ⊦ x + [] = x; (s) ⊦ ¬ a ∈ []; (s) ⊦ ¬ a ∈ x → (x + a ' = y + a ' + z ↔ y = x ∧ z = []); (ws) ni: ⊦ x + a ' = y + z ∧ ¬ a ∈ z → z = []; (forward) from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ x + a ' = y + b ' ↔ x = y ∧ a = b; (ws) ⊦ x + a ' ≠ []; (s) ⊦ x = y + a ' + z → a ∈ x; (s) in-13: ⊦ x = y + a ' + z → a ∈ x; (forward) from specification list ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ b ' ↔ a = b; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: z

Proof step 4 from proof in-09 (previous step) (back to tree)

A spec-lemma