[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Reasoning about queues
I would like to know if someone has a good theory of queues.
I would like one that is built in such a way that allows good use of
rewriting (i.e. doesn't get (grind) into infinite rewriting loops).
(I need FIFO unbounded queues for objects of any nonempty type).
I am trying with a definitional style based on finite_sequence,
but I was thinking an axiomatic style might lead to more efficient proofs.