Defining multiple expressions and corresponding alignments

[marta zhango]

I have two elisp exprossions that I want to claim are equivalent

THEOREM Expressions E1 and E2 are equivalent (E1 = E2)

ASSUME     E1 == (cons extn 'sh-mode)

                 /\ E2 == `(,(eval extn) . sh-mode)

Are the expression names E1 and E1  aligned when using the /\ notation

to define two expressions?

[Stephan Merz]

Definitions are not formulas and can therefore not appear in a conjunction.

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 visit https://groups.google.com/d/msgid/tlaplus/ed4d67bc-9c98-4d22-b6a2-aef1913c31adn%40googlegroups.com.

[marta zhango]

Then, assumptions are just set one after the other?

Example

ASSUME     A1 == (cons extn 'sh-mode)

                    A2 == `(,(eval extn) . sh-mode)

                    A3 == extn \in Vars
                       (* extn is a variable that can be evaluated *)
                    A4 == (EX v \in VALUE: ,(eval extn) = v)
                       (* Evaluation of extn results in a value v *)

[Stephan Merz]

Definitions appear one after the other. An ASSUME clause asserts a formula (which may be a conjunction), and it can be named as in

ASSUME A ==

   /\ …

   /\ …

A module may contain several ASSUME clauses.

I am not able to read the right-hand sides of your definitions, which are clearly not in TLA+ syntax.

Stephan

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/ca79ff6c-9f86-4e5f-90cd-52c55d1f2345n%40googlegroups.com.

[marta zhango]

I have the commands in emacs lisp and would like to see how one might

typically  write them in TLA+.  

Looking at

https://lamport.azurewebsites.net/tla/PConProof.pdf

I see that sometimes proofs use the hierarchy style <1> 2., <1> 3., <1> 4.

such on page 7.  But there is also the one with the  BEGIN TRANSLATION

and END TRANSLATION.