ADT LGenerator [  ]

INITIALS
nil_LGenerator:                                  -> LGenerator

CONSTRUCTORS
cons_LGenerator: Generator * LGenerator           -> LGenerator

SELECTORS
head_LGenerator   : LGenerator(i)                    -> Generator
tail_LGenerator   : LGenerator(i)                    -> LGenerator
length_LGenerator   : LGenerator(i)                    -> NAT
concat_LGenerator   : LGenerator(i) * LGenerator       -> LGenerator
isEmptyList_LGenerator   : LGenerator(i)                    -> BOOL
EQ_LGenerator(c): LGenerator(i) * LGenerator(i)    -> BOOL

AXIOMS

head_LGenerator(nil_LGenerator) = ERROR
head_LGenerator(cons_LGenerator(X1,L2)) = X1

tail_LGenerator(nil_LGenerator) = ERROR
tail_LGenerator(cons_LGenerator(X1,L2)) = L2

length_LGenerator(nil_LGenerator) = ZERO
length_LGenerator(cons_LGenerator(X1,L2)) = SUC(length_LGenerator(L2))

concat_LGenerator(nil_LGenerator,L1) = L1
concat_LGenerator(cons_LGenerator(X1,L2),L3) = cons_LGenerator(X1,concat_LGenerator(L2,L3))

isEmptyList_LGenerator(nil_LGenerator) = TRUE
isEmptyList_LGenerator(cons_LGenerator(X1,L2)) = FALSE

EQ_LGenerator(nil_LGenerator,nil_LGenerator) = TRUE
EQ_LGenerator(nil_LGenerator,cons_LGenerator(X1,L2)) = FALSE
EQ_LGenerator(cons_LGenerator(X1,L2),nil_LGenerator) = FALSE
EQ_LGenerator(cons_LGenerator(X1,L2),cons_LGenerator(X3,L4)) = AND(EQ_Generator(X1,X3),EQ_LGenerator(L2,L4))