Thanks for the reply, Andrew!
and project those behaviours to a subset of A's variables (optionally with consistent renaming)
This might be the point that I was missing. However, I'm not sure whether I really understand it. Does it mean something like implication and equivalence are "parameterized by a set of variables"? In my initial example, this could mean that CounterUp and RandomH are equivalent with respect to the variable counter and RandomH and Random are equivalent with respect to the variable choice. And because these two equivalences are "two different kinds of equivalence", the equivalence is not transitive and CounterUp is not equivalent to Random? This would intuitively make sense. Is a formal definition for implication that captures this aspect written up somewhere? Matthias -- 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/665ceefb-3f2a-03df-caa7-9217f08aafaf%40kit.edu.
Attachment:
smime.p7s
Description: S/MIME Cryptographic Signature