Selected Objects

def	res_all	res_all('a;x.P(x);x.Q(x)) == x:'a. P(x)  Q(x)
def	res_exists	res_exists('a;x.P(x);x.Q(x)) == x:'a. P(x) & Q(x)
def	res_choose	res_choose('a;x.P(x);x.Q(x)) == @x:'a. (P(x) & Q(x))
def	res_lambda	res_lambda('a;'b;x.P(x);x.f(x)) == x:'a. if P(x) then f(x) else arb('b) fi
def	hres_forall	res_forall == P:'a. Q:'a. res_all('a;x.(P(x));x.(Q(x)))
def	hres_exists	res_exists == P:'a. Q:'a. res_exists('a;x.(P(x));x.(Q(x)))
def	hres_select	res_select == P:'a. Q:'a. res_choose('a;x.(P(x));x.(Q(x)))
def	harb	arb == arb('a)
def	hres_abstract	res_abstract == P:'a. f:'a'b. res_lambda('a;'b;x.P(x);x.f(x))
THM	hres_forall_wd	'a:S.  all (P:'a  hbool. all (P:'a  hbool. (B:'a  hbool. equal (P:'a  hbool. (B:'a  hbool. (res_forall(P,B) (P:'a  hbool. (B:'a  hbool. ,all(x:'a. implies(P(x),B(x))))))
THM	hres_exists_wd	'a:S.  all (P:'a  hbool. all (P:'a  hbool. (B:'a  hbool. equal (P:'a  hbool. (B:'a  hbool. (res_exists(P,B) (P:'a  hbool. (B:'a  hbool. ,exists(x:'a. and(P(x),B(x))))))
THM	hres_select_wd	'a:S.  all (P:'a  hbool. all (P:'a  hbool. (B:'a  hbool. equal (P:'a  hbool. (B:'a  hbool. (res_select(P,B) (P:'a  hbool. (B:'a  hbool. ,select(x:'a. and(P(x),B(x))))))
THM	harb_wd	'a:S. equal(arb,select(x:'a. t))
THM	hres_abstract_wd	'a,'b:S. all (P:'a  hbool. all (P:'a  hbool. (B:'a  'b. equal (P:'a  hbool. (B:'a  'b. (res_abstract(P,B) (P:'a  hbool. (B:'a  'b. ,x:'a. cond(P(x),B(x),arb))))

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html