ADT LCasePMCaml [  ]

INITIALS
nil_LCasePMCaml:                                  -> LCasePMCaml

CONSTRUCTORS
cons_LCasePMCaml: CasePMCaml * LCasePMCaml         -> LCasePMCaml

SELECTORS
head_LCasePMCaml   : LCasePMCaml(i)                   -> CasePMCaml
tail_LCasePMCaml   : LCasePMCaml(i)                   -> LCasePMCaml
length_LCasePMCaml   : LCasePMCaml(i)                   -> NAT
concat_LCasePMCaml   : LCasePMCaml(i) * LCasePMCaml     -> LCasePMCaml
memberList_LCasePMCaml   : LCasePMCaml(i) * CasePMCaml      -> BOOL
isEmptyList_LCasePMCaml   : LCasePMCaml(i)                   -> BOOL
StringOfLCasePMCaml(c):  LCasePMCaml(i)  -> String
EQ_LCasePMCaml(c): LCasePMCaml(i) * LCasePMCaml(i)  -> BOOL

AXIOMS

head_LCasePMCaml(nil_LCasePMCaml) = ERROR
head_LCasePMCaml(cons_LCasePMCaml(X1,L2)) = X1

tail_LCasePMCaml(nil_LCasePMCaml) = ERROR
tail_LCasePMCaml(cons_LCasePMCaml(X1,L2)) = L2

length_LCasePMCaml(nil_LCasePMCaml) = ZERO
length_LCasePMCaml(cons_LCasePMCaml(X1,L2)) = SUC(length_LCasePMCaml(L2))

concat_LCasePMCaml(nil_LCasePMCaml,L1) = L1
concat_LCasePMCaml(cons_LCasePMCaml(X1,L2),L3) = cons_LCasePMCaml(X1,concat_LCasePMCaml(L2,L3))

memberList_LCasePMCaml(nil_LCasePMCaml,X1) = FALSE
memberList_LCasePMCaml(cons_LCasePMCaml(X1,L2),X3) = if EQ_CasePMCaml(X1,X3)
                                                          then TRUE
                                                          else memberList_LCasePMCaml(L2,X3)
                                                     fi

isEmptyList_LCasePMCaml(nil_LCasePMCaml) = TRUE
isEmptyList_LCasePMCaml(cons_LCasePMCaml(X1,L2)) = FALSE

StringOfLCasePMCaml(nil_LCasePMCaml) = ""
StringOfLCasePMCaml(cons_LCasePMCaml(p1,nil_LCasePMCaml)) =
  StringOfCasePMCaml(p1)
StringOfLCasePMCaml(cons_LCasePMCaml(p1,
	cons_LCasePMCaml(p2,t))) =
	concat_String(StringOfCasePMCaml(p1),
	concat_String(" |\n ",StringOfLCasePMCaml(cons_LCasePMCaml(p2,t))))

EQ_LCasePMCaml(nil_LCasePMCaml,nil_LCasePMCaml) = TRUE
EQ_LCasePMCaml(nil_LCasePMCaml,cons_LCasePMCaml(X1,L2)) = FALSE
EQ_LCasePMCaml(cons_LCasePMCaml(X1,L2),nil_LCasePMCaml) = FALSE
EQ_LCasePMCaml(cons_LCasePMCaml(X1,L2),cons_LCasePMCaml(X3,L4)) = AND(EQ_CasePMCaml(X1,X3),EQ_LCasePMCaml(L2,L4))