ADT LLabelPatternCaml [  ]

INITIALS
nil_LLabelPatternCaml:                                  -> LLabelPatternCaml

CONSTRUCTORS
cons_LLabelPatternCaml: LabelPatternCaml * LLabelPatternCaml -> LLabelPatternCaml

SELECTORS
head_LLabelPatternCaml   : LLabelPatternCaml(i)             -> LabelPatternCaml
tail_LLabelPatternCaml   : LLabelPatternCaml(i)             -> LLabelPatternCaml
length_LLabelPatternCaml   : LLabelPatternCaml(i)             -> NAT
concat_LLabelPatternCaml   : LLabelPatternCaml(i) * LLabelPatternCaml  -> LLabelPatternCaml
memberList_LLabelPatternCaml   : LLabelPatternCaml(i) * LabelPatternCaml  -> BOOL
isEmptyList_LLabelPatternCaml   : LLabelPatternCaml(i)             -> BOOL
StringOfLLabelPatternCaml  : LLabelPatternCaml(i)             -> String
EQ_LLabelPatternCaml(c): LLabelPatternCaml(i) * LLabelPatternCaml(i)  -> BOOL

AXIOMS

head_LLabelPatternCaml(nil_LLabelPatternCaml) = ERROR
head_LLabelPatternCaml(cons_LLabelPatternCaml(X1,L2)) = X1

tail_LLabelPatternCaml(nil_LLabelPatternCaml) = ERROR
tail_LLabelPatternCaml(cons_LLabelPatternCaml(X1,L2)) = L2

length_LLabelPatternCaml(nil_LLabelPatternCaml) = ZERO
length_LLabelPatternCaml(cons_LLabelPatternCaml(X1,L2)) = SUC(length_LLabelPatternCaml(L2))

concat_LLabelPatternCaml(nil_LLabelPatternCaml,L1) = L1
concat_LLabelPatternCaml(cons_LLabelPatternCaml(X1,L2),L3) = cons_LLabelPatternCaml(X1,concat_LLabelPatternCaml(L2,L3))

memberList_LLabelPatternCaml(nil_LLabelPatternCaml,X1) = FALSE
memberList_LLabelPatternCaml(cons_LLabelPatternCaml(X1,L2),X3) = if EQ_LabelPatternCaml(X1,X3)
                                                                      then TRUE
                                                                      else memberList_LLabelPatternCaml(L2,X3)
                                                                 fi

isEmptyList_LLabelPatternCaml(nil_LLabelPatternCaml) = TRUE
isEmptyList_LLabelPatternCaml(cons_LLabelPatternCaml(X1,L2)) = FALSE

StringOfLLabelPatternCaml(nil_LLabelPatternCaml) = ""
StringOfLLabelPatternCaml(cons_LLabelPatternCaml(lp1,nil_LLabelPatternCaml)) =
  StringOfLabelPatternCaml(lp1)
StringOfLLabelPatternCaml(cons_LLabelPatternCaml(lp1,
	cons_LLabelPatternCaml(lp2,t))) =
	concat_String("(",
	concat_String(StringOfLabelPatternCaml(lp1),
	concat_String(")",StringOfLLabelPatternCaml(cons_LLabelPatternCaml(lp2,t)))))
	


EQ_LLabelPatternCaml(nil_LLabelPatternCaml,nil_LLabelPatternCaml) = TRUE
EQ_LLabelPatternCaml(nil_LLabelPatternCaml,cons_LLabelPatternCaml(X1,L2)) = FALSE
EQ_LLabelPatternCaml(cons_LLabelPatternCaml(X1,L2),nil_LLabelPatternCaml) = FALSE
EQ_LLabelPatternCaml(cons_LLabelPatternCaml(X1,L2),cons_LLabelPatternCaml(X3,L4)) = AND(EQ_LabelPatternCaml(X1,X3),EQ_LLabelPatternCaml(L2,L4))