ADT Axiom [ ] INITIALS axiom : Expr * Expr -> Axiom CONSTRUCTORS SELECTORS leftAxiom : Axiom(i) -> Expr rightAxiom : Axiom(i) -> Expr EQ_Axiom (c): Axiom(i) * Axiom(i) -> BOOL AXIOMS leftAxiom(axiom(E1,E2)) = E1 rightAxiom(axiom(E1,E2)) = E2 EQ_Axiom(axiom(E1,E2),axiom(E3,E4)) = AND(EQ_Expr(E1,E3),EQ_Expr(E2,E4))