The system consists of two processes called Inc and Dec. The processes share integer variable x. Process Inc repeatedly increments x, and process Dec decrements x if another boolean variable flag is true. Variable x is initially 0 and variable falg is initially false. Variable flag is set to true by process Inc if  the process increments variable x and variable flag is set to false by process Dec if the process decrements variable x.

- incdec.mod           CafeOBJ specification of the system.
- invariants.mod      Invariants to prove.
- template.mod        Proof scores templates.
- proof100.mod        Proof score of Claim 100.
- proof110.mod        Proof score of Claim 110.