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