/* Modified by ManTa 3.3 preprocessor.  Version 1.0 */

ADT String [  ]

INITIALS
nil_String  :                                  -> String

CONSTRUCTORS
cons_String : Char * String                    -> String

SELECTORS
head_String   : String(i)                        -> Char
tail_String   : String(i)                        -> String
length_String   : String(i)                        -> NAT
concat_String   : String(i) * String               -> String
isEmptyList_String   : String(i)                        -> BOOL
EQ_String(c): String(i) * String(i)            -> BOOL

AXIOMS

head_String(nil_String) = ERROR
head_String(cons_String(X1,L2)) = X1

tail_String(nil_String) = ERROR
tail_String(cons_String(X1,L2)) = L2

length_String(nil_String) = ZERO
length_String(cons_String(X1,L2)) = SUC(length_String(L2))

concat_String(nil_String,L1) = L1
concat_String(cons_String(X1,L2),L3) = cons_String(X1,concat_String(L2,L3))

isEmptyList_String(nil_String) = TRUE
isEmptyList_String(cons_String(X1,L2)) = FALSE

EQ_String(nil_String,nil_String) = TRUE
EQ_String(nil_String,cons_String(X1,L2)) = FALSE
EQ_String(cons_String(X1,L2),nil_String) = FALSE
EQ_String(cons_String(X1,L2),cons_String(X3,L4)) = AND(EQ_Char(X1,X3),EQ_String(L2,L4))