infix L o R = L /\ ()R; infix L * R = L U R; op TICK R = t o ((- t) * R); op Phi1 = [] - b; op Phi2 = (-b) * (b o ((-t) * (TICK (TICK (TICK (TICK (a o T))))))); (Phi1 \/ Phi2) => ([] - error); ([] - error) => (Phi1 \/ Phi2);