Selected Objects

def	b_exists_unique	b_exists_unique('a;x.p(x)) == (x:'a. p(x))(x,y:'a.  (p(x)p(y))(x = y))
THM	assert_of_b_exists_unique	p:('a).  b_exists_unique('a;x.p(x))  (x:'a. p(x)) & (x,y:'a. p(x) & p(y)  x = y)
def	one_one	one_one('a;'b;f) == x,y:'a. f(x) = f(y)  'b  x = y
def	onto	onto('a;'b;f) == y:'b. x:'a. y = f(x)
def	hexists	exists == p:'a. x:'a. (p(x))
def	ht	t == true
def	hall	all == p:'a. x:'a. (p(x))
def	hand	and == p:. q:. pq
def	hor	or == p:. q:. p  q
def	hf	f == false
def	hnot	not == p:. p
def	hexists_unique	exists_unique == p:'a. b_exists_unique('a;x.p(x))
def	hlet	let == f:'a'b. e:'a. let x = e in f(x)
def	hcond	cond == b:. p:'a. q:'a. if b then p else q fi
def	hone_one	one_one == f:'a'b. one_one('a;'b;f)
def	honto	onto == f:'a'b. onto('a;'b;f)
def	htype_definition	type_definition == P:'a. rep:'b'a. type_definition('a;'b;P;rep)
THM	hexists_def	'a:S. equal(exists,P:'a  hbool. P(select(P)))
THM	htruth	equal(t,equal((x:hbool. x),x:hbool. x))
THM	hforall_def	'a:S. equal(all,P:'a  hbool. equal(P,x:'a. t))
THM	hand_def	equal (and ,t1:hbool. t2:hbool. all(t:hbool. implies(implies(t1,implies(t2,t)),t)))
THM	hor_def	equal (or ,t1:hbool. t2:hbool. all ,t1:hbool. t2:hbool. (t:hbool. implies ,t1:hbool. t2:hbool. (t:hbool. (implies(t1,t) ,t1:hbool. t2:hbool. (t:hbool. ,implies(implies(t2,t),t))))
THM	hf_def	equal(f,all(t:hbool. t))
THM	hnot_def	equal(not,t:hbool. implies(t,f))
THM	hexists_unique_def	'a:S.  equal (exists_unique ,P:'a  hbool. and ,P:'a  hbool. (exists(P) ,P:'a  hbool. ,all(x:'a. all(y:'a. implies(and(P(x),P(y)),equal(x,y))))))
THM	hlet_def	'b,'a:S. equal(let,f:'a  'b. x:'a. f(x))
THM	hcond_def	'a:S.  equal (cond ,t:hbool. t1:'a. t2:'a. select ,t:hbool. t1:'a. t2:'a. (x:'a. and ,t:hbool. t1:'a. t2:'a. (x:'a. (implies(equal(t,t),equal(x,t1)) ,t:hbool. t1:'a. t2:'a. (x:'a. ,implies(equal(t,f),equal(x,t2)))))
THM	hone_one_def	'b,'a:S. all (f:'a  'b. equal (f:'a  'b. (one_one(f) (f:'a  'b. ,all (f:'a  'b. ,(x1:'a. all(x2:'a. implies(equal(f(x1),f(x2)),equal(x1,x2))))))
THM	honto_def	'a,'b:S. all(f:'a  'b. equal(onto(f),all(y:'b. exists(x:'a. equal(y,f(x))))))
THM	htype_definition_wd	'b,'a:S. all (P:'a  hbool. all (P:'a  hbool. (rep:'b  'a. equal (P:'a  hbool. (rep:'b  'a. (type_definition(P,rep) (P:'a  hbool. (rep:'b  'a. ,and (P:'a  hbool. (rep:'b  'a. ,(all (P:'a  hbool. (rep:'b  'a. ,((x':'b. all (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. implies (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. (equal(rep(x'),rep(x'')) (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. ,equal(x',x'')))) (P:'a  hbool. (rep:'b  'a. ,,all (P:'a  hbool. (rep:'b  'a. ,,(x:'a. equal (P:'a  hbool. (rep:'b  'a. ,,(x:'a. (P(x) (P:'a  hbool. (rep:'b  'a. ,,(x:'a. ,exists (P:'a  hbool. (rep:'b  'a. ,,(x:'a. ,(x':'b. equal(x,rep(x')))))))))
THM	hbool_cases_ax	all(t:hbool. or(equal(t,t),equal(t,f)))
THM	himp_antisym_ax	all (t1:hbool. all (t1:hbool. (t2:hbool. implies (t1:hbool. (t2:hbool. (implies(t1,t2) (t1:hbool. (t2:hbool. ,implies(implies(t2,t1),equal(t1,t2)))))
THM	heta_ax	'b,'a:S. all(t:'a  'b. equal((x:'a. t(x)),t))
THM	hselect_ax	'a:S. all(P:'a  hbool. all(x:'a. implies(P(x),P(select(P)))))
THM	hinfinity_ax	exists(f:hind  hind. and(one_one(f),not(onto(f))))
THM	band_simp_1	b:. (btrue) = b
THM	bor_simp_1	b:. (b  true) = true
THM	bor_simp_2	b:. (b  false) = b
THM	bor_simp_3	b:. (true  b) = true
THM	bor_simp_4	b:. (false  b) = b
THM	band_simp_4	b:. (falseb) = false
THM	band_simp_3	b:. (trueb) = b
THM	band_simp_2	b:. (bfalse) = false
THM	bnot_simp_1	true = false
THM	bnot_simp_2	false = true
THM	bequal_refl_simp	'a:S, x:'a. (x = x) = true
THM	equal_btrue_to_assert	p:. p = true  p
THM	equal_btrue_to_assert_2	p:. true = p  p
THM	equal_bfalse_to_assert	p:. p = false  p
THM	equal_bfalse_to_assert_2	p:. false = p  p
THM	bexists_btrue	'a:S. (x:'a. true) = true
THM	bexists_bfalse	'a:S. (x:'a. false) = false
THM	ball_btrue	'a:S. (x:'a. true) = true
THM	ball_bfalse	'a:S. (x:'a. false) = false

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