# [tlaplus] TLA Proof System - the syntax has impact on provability ?


Hello,

I have example of two lemmas which have the same meaning but slightly differs in the syntax.

LEMMA lemma1 == C = {[s|->0]}
/\
D = {[s|->x.s] : x \in C}
=>
C = {[s|->x.s] : x \in D}
OBVIOUS

LEMMA lemma2 == C = [s : {0}]
/\
D = {[s|->x.s] : x \in C}
=>
C = {[s|->x.s] : x \in D}
OBVIOUS

lemma1 has been proved by "TLA - Isabelle", but "TLA - SMT", "TLA - Zenon", "TLA - Isabelle" fail to prove lemma2.

I don't understand why TLA proof system fails to prove lemma2, which is different from lemma1 only in the syntax of TLA records. Meaning:

C = {[s|->0]}
and
C = [s : {0}]

which are the same for me.

Harold

--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.