// A library for "plus" operator on natural numbers:

// Type "natural number":
TYPE nat

// Declaration for "plus":
SIGN plus : nat nat -> nat (prior = 5, notation = _+_)

// Rewrite Rule for commutativity:
RR comm  (PARAMS mīnat, nīnat)
	   m+n --> n+m

// Rewrite Rules for associativity:
RR assoc1 (PARAMS līnat, mīnat, nīnat)
	    l+(m+n) --> (l+m)+n
RR assoc2 (PARAMS līnat, mīnat, nīnat)
	    (l+m)+n --> l+(m+n)