[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Obtaining Actual Proof Found when using TLAPS? Why is associativity not built-in?





LEMMA \A n \in Nat : (\E m \in Nat : n = m+m) => n \div 2 = 0

fails

Well, fortunately TLAPS fails to prove this ... I meant to write

LEMMA \A n \in Nat : (\E m \in Nat : n = m+m) => n % 2 = 0

which is indeed proved by OBVIOUS. Still, there are many intuitively obvious facts that TLAPS fails to prove: for example, it will not prove essentially any assertion involving the Cardinality operator.

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/e7535dbc-0eeb-49a4-ba50-aac7a35bc9dfn%40googlegroups.com.