mod* GROUP{ 
[Group]
op 0 : -> Group
op _+_ : Group Group -> Group
op -_ : Group -> Group
vars X Y Z : Group
eq [lid] : 0 + X = X .
eq [linv] : (- X) + X = 0 .
eq [assoc] : X + (Y + Z) = (X + Y) + Z . 
}

-- Lemma GROUP |= forall x. x + 0 = x 
-- Proof:
-- Solution 1
open GROUP + EQL
vars X Y Z : Group .
eq [rinv] : X + (- X) = 0 .
op a : -> Group .
start a + 0 = a .
apply -.linv with X = a at (1 2) .
**> result a + (- a + a) = a : Bool
apply assoc at (1) .
**> result (a + (- a)) + a = a : Bool
apply red at term .
**> result true : Bool
close

mod* PNAT { 
[Nat]
op 0 : -> Nat {constr} 
op s_ : Nat -> Nat {constr} 
op _+_ : Nat Nat -> Nat
vars X Y : Nat
eq 0 + X = X .
eq s X + Y = s (X + Y) . 
}


mod* SPEC { 
[Elt]
ops a b : -> Elt
op _=_ : Elt Elt -> Bool
vars X Y : Elt
eq [equal] : (X = X) = true .
ceq [cequal] : X = Y if (X = Y) .
}

mod* QUEUE(D :: SPEC){ 
[Queue]
op nil : -> Queue {constr} 
op _@_ : Elt Queue -> Queue {constr} 
op _in_ : Elt Queue -> Bool
op empty? : Queue -> Bool
var Q : Queue
vars X Y : Elt
eq X in nil = false .
eq X in (Y @ Q) = (X = Y) or (X in Q) .
eq empty?(nil) = true .
eq empty?(X @ Q) = false . }