ADT LDomain [  ]

INITIALS
nil_LDomain :                                  -> LDomain

CONSTRUCTORS
cons_LDomain: Domain * LDomain                 -> LDomain

SELECTORS
head_LDomain   : LDomain(i)                       -> Domain
tail_LDomain   : LDomain(i)                       -> LDomain
length_LDomain   : LDomain(i)                       -> NAT
isEmptyList_LDomain   : LDomain(i)                       -> BOOL
EQ_LDomain(c): LDomain(i) * LDomain(i)          -> BOOL

AXIOMS

head_LDomain(nil_LDomain) = ERROR
head_LDomain(cons_LDomain(X1,L2)) = X1

tail_LDomain(nil_LDomain) = ERROR
tail_LDomain(cons_LDomain(X1,L2)) = L2

length_LDomain(nil_LDomain) = ZERO
length_LDomain(cons_LDomain(X1,L2)) = SUC(length_LDomain(L2))

isEmptyList_LDomain(nil_LDomain) = TRUE
isEmptyList_LDomain(cons_LDomain(X1,L2)) = FALSE

EQ_LDomain(nil_LDomain,nil_LDomain) = TRUE
EQ_LDomain(nil_LDomain,cons_LDomain(X1,L2)) = FALSE
EQ_LDomain(cons_LDomain(X1,L2),nil_LDomain) = FALSE
EQ_LDomain(cons_LDomain(X1,L2),cons_LDomain(X3,L4)) = AND(EQ_Domain(X1,X3),EQ_LDomain(L2,L4))