Remove redundant checks

I just moved the evaluation of each check so that we basically return from the checks as soon as one step fails. (Execute the checks in a lazy manner.)

Based on Nian-Ze's comments:

• Invariant: M |= Inv && P (invalid invariant and true)
• Safe invariant: M |= Inv then Inv => P (invalid invariant, unsafe invariant, and true)
• Safe and inductive invariant: initiation, consecution, and consistency (invalid invariant, non-inductive, unsafe invariant, and true)

Originally we talked about adding a debug mode, which would execute all checks regardless of results. But I thought about this and checked how this would look in the code - I think it would result in ugly and easy to break code, so I recommend not adding it for now.

If I need to execute all checks for debugging, I'd rather add it at that time, I am not even sure at this point if I will need that for debugging. :)

(Note: this improvement is not intended for the artifact)