ADT ListExprCaml [] INITIALS CONSTRUCTORS SELECTORS ListExprCaml_nil : -> ExprCaml ListExprCaml_cons : ExprCaml * ExprCaml -> ExprCaml ListExprCaml_head : ExprCaml -> ExprCaml ListExprCaml_tail : ExprCaml -> ExprCaml ListExprCaml_length : ExprCaml -> ExprCaml ListExprCaml_concat : ExprCaml * ExprCaml -> ExprCaml ListExprCaml_isEmptyList : ExprCaml -> ExprCaml ListExprCaml_EQ_List (c): ExprCaml * ExprCaml -> ExprCaml isList_nil: String -> BOOL isList_cons: String -> BOOL isList_head: String -> BOOL isList_tail: String -> BOOL isList_length: String -> BOOL isList_concat: String -> BOOL isList_isEmptyList: String -> BOOL isList_EQ_List: String -> BOOL List_String:->String isEmpty_String: -> String AXIOMS List_String="List" isEmpty_String="isEmpty" ListExprCaml_nil=constantEC(consCC("[]")) ListExprCaml_cons(e1,e2)=consListEC(e1,e2) ListExprCaml_head(e)=funApp(valPathEC(concat_String(List_String,".hd")),e) ListExprCaml_tail(e)=funApp(valPathEC(concat_String(List_String,".tl")),e) ListExprCaml_length(e)=funApp(valPathEC(concat_String(List_String,".length")),e) ListExprCaml_concat(e1,e2)=infixEC(e1,"@",e2) ListExprCaml_isEmptyList(e)=infixEC(e,"=",ListExprCaml_nil) ListExprCaml_EQ_List(e1,e2)=infixEC(e1,"=",e2) isList_nil(s)=EQ_String(s,"list") isList_cons(s)=EQ_String(s,"cons") isList_head(s)=EQ_String(s,"head") isList_tail(s)=EQ_String(s,"tail") isList_length(s)=EQ_String(s,"length") isList_concat(s)=EQ_String(s,"concat") isList_isEmptyList(s)=EQ_String(s,concat_String(isEmpty_String,"List")) isList_EQ_List(s)=EQ_String(s,"EQ_List")