Prove (x + y) % 3 = 0 => (10*x + y) % 3 = 0

DivideByThree.tla

---------------------------- MODULE DivideByThree ----------------------------
EXTENDS Integers

VARIABLES x, y
vars == <<x, y>>

Init == /\ x \in 1..9
        /\ y \in 0..9

Next == \//\ x' = x + 1
          /\ x' < 10
          /\ UNCHANGED <<y>>
        \//\ y' = y + 1
          /\ y' < 10
          /\ UNCHANGED <<x>>

\* TLC considers a reachable state from which there is no next
\* state satisfying the next-state action to be a deadlock error. 
\* Termination is the deadlock that we want to happen. We need to
\* tell TLC to ignore deadlock by unchecking the Deadlock box in the What
\* to check section of the model overview page.

TypeOK == (x + y) % 3 = 0 => (10*x + y) % 3 = 0

Spec == Init /\ [][Next]_vars

=============================================================================
\* Modification History
\* Last modified Tue Jul 14 10:43:38 CST 2015 by jian
\* Created Tue Jul 14 10:07:49 CST 2015 by jian