ADT LTypeRepCaml [  ]

INITIALS
nil_LTypeRepCaml:                                  -> LTypeRepCaml

CONSTRUCTORS
cons_LTypeRepCaml: TypeRepCaml * LTypeRepCaml       -> LTypeRepCaml

SELECTORS
head_LTypeRepCaml   : LTypeRepCaml(i)                  -> TypeRepCaml
tail_LTypeRepCaml   : LTypeRepCaml(i)                  -> LTypeRepCaml
length_LTypeRepCaml   : LTypeRepCaml(i)                  -> NAT
concat_LTypeRepCaml   : LTypeRepCaml(i) * LTypeRepCaml   -> LTypeRepCaml
memberList_LTypeRepCaml   : LTypeRepCaml(i) * TypeRepCaml    -> BOOL
isEmptyList_LTypeRepCaml   : LTypeRepCaml(i)                  -> BOOL
StringOfLTypeRepCaml:LTypeRepCaml(i)*String-> String
EQ_LTypeRepCaml(c): LTypeRepCaml(i) * LTypeRepCaml(i)  -> BOOL

AXIOMS

head_LTypeRepCaml(nil_LTypeRepCaml) = ERROR
head_LTypeRepCaml(cons_LTypeRepCaml(X1,L2)) = X1

tail_LTypeRepCaml(nil_LTypeRepCaml) = ERROR
tail_LTypeRepCaml(cons_LTypeRepCaml(X1,L2)) = L2

length_LTypeRepCaml(nil_LTypeRepCaml) = ZERO
length_LTypeRepCaml(cons_LTypeRepCaml(X1,L2)) = SUC(length_LTypeRepCaml(L2))

concat_LTypeRepCaml(nil_LTypeRepCaml,L1) = L1
concat_LTypeRepCaml(cons_LTypeRepCaml(X1,L2),L3) = cons_LTypeRepCaml(X1,concat_LTypeRepCaml(L2,L3))

memberList_LTypeRepCaml(nil_LTypeRepCaml,X1) = FALSE
memberList_LTypeRepCaml(cons_LTypeRepCaml(X1,L2),X3) = if EQ_TypeRepCaml(X1,X3)
                                                            then TRUE
                                                            else memberList_LTypeRepCaml(L2,X3)
                                                       fi

isEmptyList_LTypeRepCaml(nil_LTypeRepCaml) = TRUE
isEmptyList_LTypeRepCaml(cons_LTypeRepCaml(X1,L2)) = FALSE

StringOfLTypeRepCaml(nil_LTypeRepCaml,S1)=""
StringOfLTypeRepCaml(cons_LTypeRepCaml(T1,nil_LTypeRepCaml),S3)=
  StringOfTypeRepCaml(T1)
StringOfLTypeRepCaml(cons_LTypeRepCaml(T1,cons_LTypeRepCaml(T2,rem)),S3)=
  concat_String(StringOfTypeRepCaml(T1),
  concat_String(S3,
    StringOfLTypeRepCaml(cons_LTypeRepCaml(T2,rem),S3)))

EQ_LTypeRepCaml(nil_LTypeRepCaml,nil_LTypeRepCaml) = TRUE
EQ_LTypeRepCaml(nil_LTypeRepCaml,cons_LTypeRepCaml(X1,L2)) = FALSE
EQ_LTypeRepCaml(cons_LTypeRepCaml(X1,L2),nil_LTypeRepCaml) = FALSE
EQ_LTypeRepCaml(cons_LTypeRepCaml(X1,L2),cons_LTypeRepCaml(X3,L4)) = AND(EQ_TypeRepCaml(X1,X3),EQ_LTypeRepCaml(L2,L4))