Re: [tlaplus] Record Equality

[Stephan Merz <stephan.merz@xxxxxxxxx>]

Hi Saksham,

your lemma is valid: the second conjunct on the left of the implication is superfluous but certainly does not invalidate the lemma (if A => B then a fortiori also A /\ X => B).

Best,

Stephan

On 20 Aug 2019, at 17:49, Saksham Chand <schand@xxxxxxxxxxxxxxxxx> wrote:

Hi,

I'm running TLAPS 1.6 (TLAPM 1.4.3) and the following is discharged by the proof system. Is this expected or a bug?

LEMMA RecordEquality == \A d1, d2 \in [slot: Nat]:
        /\ d1.slot = d2.slot
        /\ d1.val = d2.val
        => d1 = d2 BY Isa

Thanks,

Saksham

--
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/CAJSuO--qCj9PrYf4riCOiwB71%2BusQ%3DXgVTO-Y4wkcQxfNG-qJw%40mail.gmail.com.

--
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/DC14F59C-1F63-4E8F-8648-E9CD76D634A9%40gmail.com.