ADT BOOL [ ] INITIALS TRUE : -> BOOL FALSE : -> BOOL CONSTRUCTORS SELECTORS AND (c): BOOL * BOOL(i) -> BOOL OR (c): BOOL * BOOL(i) -> BOOL NOT (c): BOOL(i) -> BOOL IMP (c): BOOL(i) * BOOL(i) -> BOOL EQ_BOOL (c): BOOL(i) * BOOL(i) -> BOOL AXIOMS AND(B1,TRUE) = B1 AND(B1,FALSE) = FALSE OR(B1,TRUE) = TRUE OR(B1,FALSE) = B1 NOT(TRUE) = FALSE NOT(FALSE) = TRUE IMP(TRUE,TRUE) = TRUE IMP(TRUE,FALSE) = FALSE IMP(FALSE,TRUE) = TRUE IMP(FALSE,FALSE) = TRUE EQ_BOOL(TRUE,TRUE) = TRUE EQ_BOOL(TRUE,FALSE) = FALSE EQ_BOOL(FALSE,TRUE) = FALSE EQ_BOOL(FALSE,FALSE) = TRUE