ADT LSelector [ ] INITIALS nil_LSelector: -> LSelector CONSTRUCTORS cons_LSelector: Selector * LSelector -> LSelector SELECTORS head_LSelector : LSelector(i) -> Selector tail_LSelector : LSelector(i) -> LSelector length_LSelector : LSelector(i) -> NAT isEmptyList_LSelector : LSelector(i) -> BOOL EQ_LSelector(c): LSelector(i) * LSelector(i) -> BOOL AXIOMS head_LSelector(nil_LSelector) = ERROR head_LSelector(cons_LSelector(X1,L2)) = X1 tail_LSelector(nil_LSelector) = ERROR tail_LSelector(cons_LSelector(X1,L2)) = L2 length_LSelector(nil_LSelector) = ZERO length_LSelector(cons_LSelector(X1,L2)) = SUC(length_LSelector(L2)) isEmptyList_LSelector(nil_LSelector) = TRUE isEmptyList_LSelector(cons_LSelector(X1,L2)) = FALSE EQ_LSelector(nil_LSelector,nil_LSelector) = TRUE EQ_LSelector(nil_LSelector,cons_LSelector(X1,L2)) = FALSE EQ_LSelector(cons_LSelector(X1,L2),nil_LSelector) = FALSE EQ_LSelector(cons_LSelector(X1,L2),cons_LSelector(X3,L4)) = AND(EQ_Selector(X1,X3),EQ_LSelector(L2,L4))