SIGNATURE BitsetReduce[to]

--

-- Parameter
SORT to

IMPORT Bitset ONLY set
       Nat ONLY nat

FUN / : (nat ** to -> to) ** to ** set -> to
        -- (o, e)/ s
        -- reduce s by o with value e as initial 2nd argument
        -- function f should be left-commutative:  x o (y o z) = y o (x o z)
        -- since reduction order is implementation dependent and should 
        -- not be relevant!
        -- informally:
        -- (o / e)({a,b,...,y,z}) == a o (b o (...(y o (z o e))...))