The system consists of two processes called Parent and Child. They share a bank account acc. Parent repeatedly adds some amount to the account. Child subtracts some amount from the account provided that the balance never gets negative.

1. Make a formal model of this system as a transition system and describe it in CafeOBJ.
2. Write proof scores in CafeOBJ showing that acc is always equal to or greater than 0.