ADT List [ X ]

INITIALS
nil         :                                  -> List

CONSTRUCTORS
cons        : X * List                         -> List

SELECTORS
head        : List(i)                          -> X
tail        : List(i)                          -> List
length      : List(i)                          -> NAT
concat      : List(i) * List                   -> List
isEmptyList   : List(i)                          -> BOOL
isMemberList  : List(i) * X ->BOOL
/* Difference of two lists, returns a list with the elements
   of the first that don't appear in the second */
difList     : List(i)*List                    ->List

EQ_List  (c): List(i) * List(i)                -> BOOL

AXIOMS

head(nil) = ERROR
head(cons(X1,L2)) = X1

tail(nil) = ERROR
tail(cons(X1,L2)) = L2

length(nil) = ZERO
length(cons(X1,L2)) = SUC(length(L2))

concat(nil,L1) = L1
concat(cons(X1,L2),L3) = cons(X1,concat(L2,L3))

isEmptyList(nil) = TRUE
isEmptyList(cons(X1,L2)) = FALSE

isMemberList(nil,elem) = FALSE
isMemberList(cons(X1,L2),elem) = if EQUAL(elem,X1) then TRUE else isMemberList(L2,elem) fi

difList(nil,l2)=nil
difList(cons(h,t),l2)=
  if isMemberList(l2,h) then
    difList(t,l2)
  else
    cons(h,difList(t,l2))
  fi

EQ_List(nil,nil) = TRUE
EQ_List(nil,cons(X1,L2)) = FALSE
EQ_List(cons(X1,L2),nil) = FALSE
EQ_List(cons(X1,L2),cons(X3,L4)) = AND(EQUAL(X1,X3),EQ_List(L2,L4))