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

*From*: Calvin Loncaric <c.a.loncaric@xxxxxxxxx>*Date*: Fri, 2 Dec 2022 18:44:08 -0800*References*: <c86392a7-d2d4-4b62-935b-265874627159n@googlegroups.com>

Try adding `3 \in S` to your assumptions (along with the commented-out rule about P's behavior `\A s \in S : P[s] = IF s \in {1, 2} THEN TRUE ELSE FALSE`).

Since S is unconstrained, there is no way for you (or TLAPS) to prove or disprove either of the following:

- 3 \in S
- 3 \notin S

If `3 \in S`, then we can instantiate the rule about P's behavior to show `P[3] = IF 3 \in {1, 2} THEN TRUE ELSE FALSE`, implying `P[3] = FALSE`.

If `3 \notin S` then we can't say anything about what P[3] equals. In this case P[3] could be TRUE, even given all your other assumptions.

--

Calvin

On Fri, Dec 2, 2022 at 1:58 PM jack malkovick <sillymouse333@xxxxxxxxx> wrote:

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

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.

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/CABf5HMhf7LJbtv6NYnVSNuB7B3uqVMLyj6Jxt5thtDLQL60iag%40mail.gmail.com.

**References**:**[tlaplus] Defining functions in TLAPS***From:*jack malkovick

- Prev by Date:
**[tlaplus] Defining functions in TLAPS** - Next by Date:
**[tlaplus] TLA+ Community Meeting 2023** - Previous by thread:
**[tlaplus] Defining functions in TLAPS** - Next by thread:
**[tlaplus] TLA+ Community Meeting 2023** - Index(es):