I'm trying to understand the point of the "existential magic wand" operator.
I see that (P * Q) -o R = P -o (Q -o R), which is clearly a form of currying,
and |> (P -o Q) = |> P -o |> Q is just a distributive axiom.
The axioms ewand_TT_sepcon ((P * Q) && (R -o TT) |-- (P && (R -o TT)) * (Q && (R -o TT))), exclude_elsewhere (P * Q |-- (P && (Q -o TT)) * Q)),
and ewand_conflict (P * Q |-- FF -> P && (Q -o R) |-- FF) confuse me.
What are the intended semantics of the existential magic wand?
Finally figured it out. It's just
¬P * Q, as opposed to the usual magic wand (¬P ⅋ Q).