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.