|I think this is a matter of parsing precedence.|
\A x : M(x) = S(x) /\ ~U(x)
is parsed as
\A x : (M(x) = S(x)) /\ ~U(x)
and therefore your hypotheses imply
\A x : ~ U(x)
For the analogous reason, the hypothesis
NEW B(_), \A x : B(x) = S(x) /\ U(x)
\A x : U(x)
and now you get an inconsistent set of assumptions. Had you used "<=>" instead of "=", the result would have been different because conjunction binds more tightly than equivalence.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/81603491-C40C-4B21-854F-71FE85158AE9%40gmail.com.