[tlaplus] Checking or proving machine closure of a temporal formula

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

All the proofs of machine closure of a temporal formula I've seen are written outside of TLA, talking about things like prefixes of behaviors and other such things that can't really be expressed inside TLA. So how do you:

1. State "formula F is machine-closed" as a proposition in TLA

2. Write a proof of that theorem using functionality available in TLAPS

3. Alternatively, model-check that F is machine closed over a finite model

Is it possible to do any of these things? Thanks!

Andrew Helwer

-- 
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 visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUVOPq401185sHDHdbgkuZeagncnsTtw9265ZPVdE82MKA%40mail.gmail.com.