ADT LSpecificationCaml [  ]

INITIALS
nil_LSpecificationCaml:                                  -> LSpecificationCaml

CONSTRUCTORS
cons_LSpecificationCaml: SpecificationCaml * LSpecificationCaml -> LSpecificationCaml

SELECTORS
head_LSpecificationCaml   : LSpecificationCaml(i)            -> SpecificationCaml
tail_LSpecificationCaml   : LSpecificationCaml(i)            -> LSpecificationCaml
length_LSpecificationCaml   : LSpecificationCaml(i)            -> NAT
concat_LSpecificationCaml   : LSpecificationCaml(i) * LSpecificationCaml  -> LSpecificationCaml
isEmptyList_LSpecificationCaml   : LSpecificationCaml(i)            -> BOOL
isMemberList_LSpecificationCaml   : LSpecificationCaml(i) * SpecificationCaml  -> BOOL
StringOfLSpecificationCaml:LSpecificationCaml(i)->String
EQ_LSpecificationCaml(c): LSpecificationCaml(i) * LSpecificationCaml(i)  -> BOOL

AXIOMS

head_LSpecificationCaml(nil_LSpecificationCaml) = ERROR
head_LSpecificationCaml(cons_LSpecificationCaml(X1,L2)) = X1

tail_LSpecificationCaml(nil_LSpecificationCaml) = ERROR
tail_LSpecificationCaml(cons_LSpecificationCaml(X1,L2)) = L2

length_LSpecificationCaml(nil_LSpecificationCaml) = ZERO
length_LSpecificationCaml(cons_LSpecificationCaml(X1,L2)) = SUC(length_LSpecificationCaml(L2))

concat_LSpecificationCaml(nil_LSpecificationCaml,L1) = L1
concat_LSpecificationCaml(cons_LSpecificationCaml(X1,L2),L3) = cons_LSpecificationCaml(X1,concat_LSpecificationCaml(L2,L3))

isEmptyList_LSpecificationCaml(nil_LSpecificationCaml) = TRUE
isEmptyList_LSpecificationCaml(cons_LSpecificationCaml(X1,L2)) = FALSE

isMemberList_LSpecificationCaml(nil_LSpecificationCaml,elem) = FALSE
isMemberList_LSpecificationCaml(cons_LSpecificationCaml(X1,L2),elem) = if EQ_SpecificationCaml(elem,X1) then TRUE
                                                                       else isMemberList_LSpecificationCaml(L2,elem)
                                                                       fi                                                                           
StringOfLSpecificationCaml(nil_LSpecificationCaml) = ""
StringOfLSpecificationCaml(cons_LSpecificationCaml(X1,L2)) = 
  concat_String(StringOfSpecificationCaml(X1),
  concat_String(";;\n",StringOfLSpecificationCaml(L2)))

EQ_LSpecificationCaml(nil_LSpecificationCaml,nil_LSpecificationCaml) = TRUE
EQ_LSpecificationCaml(nil_LSpecificationCaml,cons_LSpecificationCaml(X1,L2)) = FALSE
EQ_LSpecificationCaml(cons_LSpecificationCaml(X1,L2),nil_LSpecificationCaml) = FALSE
EQ_LSpecificationCaml(cons_LSpecificationCaml(X1,L2),cons_LSpecificationCaml(X3,L4)) = AND(EQ_SpecificationCaml(X1,X3),EQ_LSpecificationCaml(L2,L4))