#include FLIST.cam

; Creation date: Fri Dec 12 10:56:58 WET 1997

STATE st   : (A-seq)-seq
  INV i(st   );

FUNC INS(a: A, b: NAT, c: NAT): VOID
PRE    p(st   ,a,b,c)
STATE  st    <- f(st   ,a,b,c)
RETURN g(st   ,a,b,c);

FUNC DEL(a: NAT, b: NAT): A
PRE    p(st   ,a,b)
STATE  st    <- f(st   ,a,b)
RETURN g(st   ,a,b);

FUNC READ(a: NAT, b: NAT): A
PRE    p(st   ,a,b)
STATE  st    <- f(st   ,a,b)
RETURN g(st   ,a,b);