#include FDMO.cam

; Creation date: Sat Dec 13 21:39:10 WET 1997

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

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

FUNC SUBONR(a: A, b: NAT): VOID
STATE  st    <- st    + let (f=lambda(x).
                               let (c=p2(x),
                                    d= if c >= b then c .- b else c)
                               in < p1(x), c >)
                        in (*->f)(st   /{a});

FUNC SELONR(a: NAT): B-set
RETURN UNION( { p1(st   [k]) | k <- dom(st   ): p2(st   [k]) >= a });