#include FDEP.cam

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

; STATE st   : A->(B-set)*C;

FUNC ADDONL(a: A, b: B-set): VOID
STATE st    <- st    + let (f=lambda(x).< p1(x) U b, p2(x) >)
                     in (*->f)(st   /{a});

FUNC NEW(a: A, b: B-set, c: C): VOID
STATE  st <- [ a -> <b,c> ] + st ;