for me both of your theorems are proved (by the SMT backend). Can you use SMT to prove simple theorems such as
ASSUME NEW x \in Int
PROVE x+1 = 1+x
or do you perhaps have a problem with your TLAPS installation?
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/9FABF4B7-4EFE-462F-9842-61E1DAAE727A%40gmail.com.