adt bool is
  functions
    true : bool
    false : bool
    and, or : bool * bool -> bool
    not : bool -> bool
  axioms
    [B1]  and(true,x) = x
    [B2]  and(false,x) = false
    [B3]  not(true) = false
    [B4]  not(false) = true
    [B5]  or(x,y) = not(and(not(x),not(y)))
  end