Hello,
the problem is that your safety property is not an inductive invariant (even with respect to the typing invariant). However, it is easy to see that the time stamps of your variables can never exceed the clock value, and so the extra guard that you added to the Inc action is actually an invariant of your specification. It even happens to be an inductive invariant.
The attached TLA+ module contains a proof of the safety property. Please see the TLAPS tutorial or other examples in the distribution for the concept and the importance of inductive invariants.
Hope this helps,
Stephan
P.S.: The constant MaxNum is (obviously) unnecessary for the prover – better add a state constraint to the model that you use for TLC instead of adding a spurious precondition in your specification. -s