ADT LTypeExprCaml [  ]

INITIALS
nil_LTypeExprCaml:                                  -> LTypeExprCaml

CONSTRUCTORS
cons_LTypeExprCaml: TypeExprCaml * LTypeExprCaml     -> LTypeExprCaml

SELECTORS
head_LTypeExprCaml   : LTypeExprCaml(i)                 -> TypeExprCaml
tail_LTypeExprCaml   : LTypeExprCaml(i)                 -> LTypeExprCaml
length_LTypeExprCaml   : LTypeExprCaml(i)                 -> NAT
concat_LTypeExprCaml   : LTypeExprCaml(i) * LTypeExprCaml  -> LTypeExprCaml
memberList_LTypeExprCaml   : LTypeExprCaml(i) * TypeExprCaml  -> BOOL
isEmptyList_LTypeExprCaml   : LTypeExprCaml(i)                 -> BOOL
StringOfLTypeExprCaml: LTypeExprCaml(i) * String  -> String
EQ_LTypeExprCaml(c): LTypeExprCaml(i) * LTypeExprCaml(i)  -> BOOL

AXIOMS

head_LTypeExprCaml(nil_LTypeExprCaml) = ERROR
head_LTypeExprCaml(cons_LTypeExprCaml(X1,L2)) = X1

tail_LTypeExprCaml(nil_LTypeExprCaml) = ERROR
tail_LTypeExprCaml(cons_LTypeExprCaml(X1,L2)) = L2

length_LTypeExprCaml(nil_LTypeExprCaml) = ZERO
length_LTypeExprCaml(cons_LTypeExprCaml(X1,L2)) = SUC(length_LTypeExprCaml(L2))

concat_LTypeExprCaml(nil_LTypeExprCaml,L1) = L1
concat_LTypeExprCaml(cons_LTypeExprCaml(X1,L2),L3) = cons_LTypeExprCaml(X1,concat_LTypeExprCaml(L2,L3))

memberList_LTypeExprCaml(nil_LTypeExprCaml,X1) = FALSE
memberList_LTypeExprCaml(cons_LTypeExprCaml(X1,L2),X3) = if EQ_TypeExprCaml(X1,X3)
                                                              then TRUE
                                                              else memberList_LTypeExprCaml(L2,X3)
                                                         fi

isEmptyList_LTypeExprCaml(nil_LTypeExprCaml) = TRUE
isEmptyList_LTypeExprCaml(cons_LTypeExprCaml(X1,L2)) = FALSE

StringOfLTypeExprCaml(nil_LTypeExprCaml,sep) = ""
StringOfLTypeExprCaml(cons_LTypeExprCaml(x,nil_LTypeExprCaml),sep) =
  StringOfTypeExprCaml(x)
StringOfLTypeExprCaml(cons_LTypeExprCaml(x,cons_LTypeExprCaml(h,t)),sep) =
  concat_String(StringOfTypeExprCaml(x),
  concat_String(sep,StringOfLTypeExprCaml(cons_LTypeExprCaml(h,t),sep)))

EQ_LTypeExprCaml(nil_LTypeExprCaml,nil_LTypeExprCaml) = TRUE
EQ_LTypeExprCaml(nil_LTypeExprCaml,cons_LTypeExprCaml(X1,L2)) = FALSE
EQ_LTypeExprCaml(cons_LTypeExprCaml(X1,L2),nil_LTypeExprCaml) = FALSE
EQ_LTypeExprCaml(cons_LTypeExprCaml(X1,L2),cons_LTypeExprCaml(X3,L4)) = AND(EQ_TypeExprCaml(X1,X3),EQ_LTypeExprCaml(L2,L4))