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

[haroldas.giedra@xxxxxxxxx]

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.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.