UP

The Theory pf

Parents

zfc

Constants

pf_hered(SETz func1 BOOL) func1 BOOL
pure_function SETz func1 BOOL

Definitions

pf_heredturnstil forall p
spot pf_hered p
equiv (forall s
spot (forall espot e memberofz fieldz s implies p e) and funz s implies p s)
pure_function turnstil forall sspot pure_function s equiv (forall pspot pf_hered p implies p s)


HOME net links © RBJ created 1999/11/04 modified 1999/11/04