divide_by_two(n) == CHOOSE k \in Nat: n=2*k
EXTENDS Integers, TLAPS, FiniteSets
divide_by_two(n) == CHOOSE k \in Nat: n=2*k
CONSTANTS N
VARIABLES x
Init == x = divide_by_two(N)
PositiveInvariant == x >= 0
ASSUME NumberAssumption == N \in {2,4,6,8,10}
THEOREM PositiveDivisionProperty == Init => PositiveInvariant <1> SUFFICES ASSUME Init PROVE PositiveInvariant OBVIOUS <1> QED BY NumberAssumption DEF Init, PositiveInvariant, divide_by_two
ASSUME NumberAssumption == N = 10
--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5d12aa41-9036-4ba4-856a-bf5070853122%40googlegroups.com.
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/NLLfoXEvxCU/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJSuO-_Wo9UhL3_Di9NpLO%2BSDLj-tuSNbLoSPObjwP_-JMKpyQ%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CACOXEhA-Z-DrYi-rjdd6o0D%2BgGLe9YBZ4-TPUf%2BF%3Dy175-10uQ%40mail.gmail.com.