Record Equality

[Saksham Chand]

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

[Stephan Merz]

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

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJSuO--qCj9PrYf4riCOiwB71%2BusQ%3DXgVTO-Y4wkcQxfNG-qJw%40mail.gmail.com.