Hi Chris, below is a simple proof in TLAPS of what I believe is your intended result. As Leslie remarked, your difficulties seem to be caused by a confusion between /\ and ^, both of which appear to denote conjunction in your module. LEMMA ASSUME NEW R \in Nat, \E a \in Nat : R = 2 * a, NEW N \in Nat, NEW VARIABLE x, x = R * N PROVE \E y \in Nat : x = 2 * y OBVIOUS Note that it doesn't matter for the validity of this lemma if x is declared as a VARIABLE or CONSTANT. And no, TLA+ is not primarily designed for reasoning about propositional logic (temporal or otherwise). Have you had a look at the Hyperbook? Regards, Stephan
