-- ========================================================================
--                   generic modules:  PNAT
-- ========================================================================

-- ========================================================================
-- a comment starts with '-- ' or '** ' and ends at the end of line
--
-- a convention for commenting:
--   '-- ' is used before the commented CafeOBJ text
--   '** ' is used after the commented CafeOBJ text
-- ========================================================================

-- ========================================================================
-- for defining state functions and predicates 
-- we need Peano Style Natural Numbers with _+_ and _>_
mod! PNAT { [Nat]
op 0 : -> Nat {constr} 
op s_ : Nat -> Nat {constr} 
-- equality over the natural numbers
eq (0 = s(Y:Nat)) = false .
eq (s(X:Nat) = s(Y:Nat)) = (X = Y) .
eq (s(X:Nat) = X) = false .
-- associative and commutative _+_
op _+_ : Nat Nat -> Nat {assoc comm} 
eq 0 + Y:Nat = Y .
eq (s X:Nat) + Y:Nat = s(X + Y) .
-- strict greater than
op _>_ : Nat Nat -> Bool .
eq (s X:Nat) > (s Y:Nat) = X > Y .
eq (s X:Nat) > 0 = true .
eq 0 > (s Y:Nat) = false .
eq X:Nat > X = false .
--
eq (s X:Nat) > X = true .
eq X:Nat > (s X) = false .
}

-- ========================================================================
provide pnat

-- ========================================================================
eof