ADT LAxiom [ ] INITIALS nil_LAxiom : -> LAxiom CONSTRUCTORS cons_LAxiom : Axiom * LAxiom -> LAxiom SELECTORS head_LAxiom : LAxiom(i) -> Axiom tail_LAxiom : LAxiom(i) -> LAxiom length_LAxiom : LAxiom(i) -> NAT isEmptyList_LAxiom : LAxiom(i) -> BOOL EQ_LAxiom(c): LAxiom(i) * LAxiom(i) -> BOOL AXIOMS head_LAxiom(nil_LAxiom) = ERROR head_LAxiom(cons_LAxiom(X1,L2)) = X1 tail_LAxiom(nil_LAxiom) = ERROR tail_LAxiom(cons_LAxiom(X1,L2)) = L2 length_LAxiom(nil_LAxiom) = ZERO length_LAxiom(cons_LAxiom(X1,L2)) = SUC(length_LAxiom(L2)) isEmptyList_LAxiom(nil_LAxiom) = TRUE isEmptyList_LAxiom(cons_LAxiom(X1,L2)) = FALSE EQ_LAxiom(nil_LAxiom,nil_LAxiom) = TRUE EQ_LAxiom(nil_LAxiom,cons_LAxiom(X1,L2)) = FALSE EQ_LAxiom(cons_LAxiom(X1,L2),nil_LAxiom) = FALSE EQ_LAxiom(cons_LAxiom(X1,L2),cons_LAxiom(X3,L4)) = AND(EQ_Axiom(X1,X3),EQ_LAxiom(L2,L4))