Type boolean [] declare constructors true() -> boolean; false() -> boolean; others not (boolean) -> boolean; and (boolean, boolean) -> boolean; or (boolean, boolean) -> boolean; implies (boolean, boolean) -> boolean; for all b, c in boolean; let not(true()) = false(); not(false()) = true(); and(true(),b) = b; and(false(),b) = false(); or(true(),b) = true(); or(false(),b) = b; implies(b,c) = or(not(b),c); end end boolean.