Boolean

spec
     Boolean =
     free type
          Boolean ::= TRUE | FALSE
     %%          intended system of representatives:
     %%          TRUE, FALSE
     ops
           NOT__ :           Boolean -> Boolean;
           __AND__, __OR__ : Boolean * Boolean -> Boolean;
     %%prec               __OR__ < __AND__
     vars
          x,y,z:Boolean
     .          NOT(FALSE)=TRUE
     .          NOT(TRUE)=FALSE
     .          FALSE AND FALSE = FALSE
     .          FALSE AND TRUE = FALSE
     .          TRUE  AND FALSE = FALSE
     .          TRUE  AND TRUE = TRUE
     .          x OR y=NOT(NOT(x) AND NOT(y))
end

view
     BooleanAlgebra_in_Boolean :
DefineBooleanAlgebra
     to Boolean =
     sort
          Elem |-> Boolean,
     ops
           0 |-> FALSE,
           1 |-> TRUE,
           __ cap __ |-> __AND__,
           __ cup __ |-> __OR__
end