| Hi Jaco, the directive "WITNESS e" quite clearly does not require proof, and by analogy (and in order to simplify the grammar) it was decided that "WITNESS e \in S" would not take a proof either but that the fact "e \in S" should follow obviously from the context. What you can do is write something like the following where the first step inserts the required fact in the context. <1>. e \in S BY ... <1>. WITNESS e \in S Personally, I tend to use WITNESS rarely but usually write something like <1>x. e \in S BY ... <1>y. P(e) BY ... <1>z. \E x \in S : P(x) BY <1>x, <1>y Regards, Stephan
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/1986E5A8-0341-431E-AF85-8443FFDAD787%40gmail.com. |