[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: jack malkovick <sillymouse333@xxxxxxxxx>*Date*: Thu, 1 Dec 2022 10:58:42 -0800 (PST)

How could I help TLAPS to prove this simple theorem?

ASSUME

NEW P(_), NEW Q(_)

PROVE

\A x : (P(x) # Q(x)) => (P(x) = ~Q(x))

PROOF

OBVIOUS

PS. it can prove with no problem the reverse implication

\A x : (P(x) = ~Q(x)) => (P(x) # Q(x))

-- 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/42656e1a-326f-4713-a373-4f639db81fdcn%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] another simple theorem***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] How can I define a sequence as part of a record's fields?** - Next by Date:
**Re: [tlaplus] another simple theorem** - Previous by thread:
**Re: [tlaplus] How can I define a sequence as part of a record's fields?** - Next by thread:
**Re: [tlaplus] another simple theorem** - Index(es):