Proof step 8 from proof restrict-add (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  @(m, m3, m4) = @(m0, m1, m2) ∨ @(m, m3, m4) ∈ as | m0 ⊦ m = m0 ∧ (@(m0, m3, m4) = @(m0, m1, m2) ∨ @(m0, m3, m4) ∈ as)

Rule argument

Additional information