[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Determinism of choose



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