Commutativity + Associativity of Addition

1. Lemmas

   PNAT |- eq N:PNat + 0 = N:PNat [metadata "lemma1"] ;

   PNAT |- eq M:PNat + s N:PNat = s(M:PNat + N:PNat) [metadata "lemma2"] ;

   See lemma.maude for a proof of the above lemmas.

2. Associativity

   PNAT |- eq (M:PNat + N:PNat) + P:PNat = N:PNat + (M:PNat + P:PNat) ;

   See assoc.maude for a proof of associativity.

3. Commutativity

   PNAT + {lemma1, lemma2} |- eq M:PNat + N:PNat = N:PNat + M:PNat ;

   See comm.maude for a proof of commutativity.