x0 + a ' + y = (y1 + a ') + y0, ∀ a, y, z, y0. x0 + a ' + y = z + a ' + y0 → a ∈ y ∨ a ∈ x0 ∨ y = y0 ∧ x0 = z
⊦ a = a0, a ∈ x0, a ∈ y, y = y0 ∧ x0 = y1
User applied rule all left
And closed the goal!
Rule argument
pos: left 2 terms: a, y, y1, y0 abort: F discard: T computed: T
Additional information
Used simplifier rules:
a: ⊦ (x + y) + z = x + y + z;
Used terms: a, y, y1, y0