How deterministic is the "choose" function? For example, in the else
clause of finite_sets sum:
sum(S,f) : RECURSIVE R =
IF (empty?(S)) THEN zero
ELSE f(choose(S)) + sum(rest(S),f)
ENDIF MEASURE (LAMBDA S,f: card(S))
how can we be sure that the element removed by 'rest' is the same
element returned from the earlier (explicit) 'choose'?
jerome