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

*From*: jack malkovick <sillymouse333@xxxxxxxxx>*Date*: Fri, 2 Dec 2022 13:58:17 -0800 (PST)

I'm experimenting again with TLPAS in order to learn stuff, and I guess this is the open/closed world problem.

I was trying to see if it's possible to define predicate P as TRUE only for value 1 and 2 and FALSE implicitly for any other value. Of course, none of the options below worked.

Is the any way to do this?

THEOREM TestFunction ==

ASSUME

NEW S,

NEW P \in [S -> BOOLEAN],

\* \A s \in S : P[s] = IF s \in {1, 2} THEN TRUE ELSE FALSE

\* P = (1 :> TRUE @@ 2 :> TRUE)

P[1], P[2]

PROVE

P[3] => FALSE

PROOF

OBVIOUS

ASSUME

NEW S,

NEW P \in [S -> BOOLEAN],

\* \A s \in S : P[s] = IF s \in {1, 2} THEN TRUE ELSE FALSE

\* P = (1 :> TRUE @@ 2 :> TRUE)

P[1], P[2]

PROVE

P[3] => FALSE

PROOF

OBVIOUS

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/c86392a7-d2d4-4b62-935b-265874627159n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Defining functions in TLAPS***From:*Calvin Loncaric

- Prev by Date:
**Re: [tlaplus] TLC report an unexpected runtime error** - Next by Date:
**Re: [tlaplus] Defining functions in TLAPS** - Previous by thread:
**Re: [tlaplus] TLC report an unexpected runtime error** - Next by thread:
**Re: [tlaplus] Defining functions in TLAPS** - Index(es):