Commutativity & associativity of the addition of natural numbers

The aim is to prove that the addition of natural numbers is both commutative and associative; that is, for any three natural numbers $m$, $n$, and $p$ we have: $$ m + n = n + m \qquad \text{and} \qquad (m + n) + p = m + (n + p) $$

Specification

See pnat.maude for the full specification.

Verification

Lemmas

To prove the commutativity and associativity of addition, we need two 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 these lemmas.

Commutativity

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

See comm.maude for a proof of the commutativity.

Associativity

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

See assoc.maude for a proof of the associativity.