Selected Objects

def	ncompose	ncompose(f;n;x) == if n=0 then x else f(ncompose(f;n-1;x)) fi   (recursive)
THM	ncompose_zero	f:('a'a), x:'a. ncompose(f;0;x) = x
THM	ncompose_pos	n:, x:'a, f:('a'a). n>0  ncompose(f;n;x) = f(ncompose(f;n-1;x))
THM	decidable__nat	m,n:. Dec(m = n)
THM	nat_eq_to_int	m,n:. m = n  m = n
def	hnum	hnum ==
def	hsuc_rep	suc_rep == x:. (@f:. (one_one(;;f) & onto(;;f)))(x)
def	hzero_rep	zero_rep == @x:. (y:. x = suc_rep(y)  )
def	his_num_rep	is_num_rep == m:. P:. ((P(zero_rep))(n:. (P(n))(P(suc_rep(n)))))(P(m))
def	hrep_num	rep_num == n:. ncompose(suc_rep;n;zero_rep)
def	habs_num	abs_num == n:. @m:. (n = rep_num(m)  )
def	hzero	zero == 0
def	hsuc	suc == n:. n+1
THM	num_iso	iso_pair(;;is_num_rep;rep_num;abs_num)
THM	hsuc_rep_def	equal(suc_rep,select(f:hind  hind. and(one_one(f),not(onto(f)))))
THM	hzero_rep_def	equal(zero_rep,select(x:hind. all(y:hind. not(equal(x,suc_rep(y))))))
THM	his_num_rep_wd	all (m:hind. equal (m:hind. (is_num_rep(m) (m:hind. ,all (m:hind. ,(P:hind  hbool. implies (m:hind. ,(P:hind  hbool. (and (m:hind. ,(P:hind  hbool. ((P(zero_rep) (m:hind. ,(P:hind  hbool. (,all(n:hind. implies(P(n),P(suc_rep(n))))) (m:hind. ,(P:hind  hbool. ,P(m)))))
THM	hnum_ty_def	exists(rep:hnum  hind. type_definition(is_num_rep,rep))
THM	hnum_iso_def	and (all(a:hnum. equal(abs_num(rep_num(a)),a)) ,all(r:hind. equal(is_num_rep(r),equal(rep_num(abs_num(r)),r))))
THM	hzero_def	equal(0,abs_num(zero_rep))
THM	hsuc_def	all(m:hnum. equal(suc(m),abs_num(suc_rep(rep_num(m)))))
THM	hnot_suc	all(n:hnum. not(equal(suc(n),0)))
THM	hinv_suc	all(m:hnum. all(n:hnum. implies(equal(suc(m),suc(n)),equal(m,n))))
THM	hinduction	all (P:hnum  hbool. implies (P:hnum  hbool. (and(P(0),all(n:hnum. implies(P(n),P(suc(n))))) (P:hnum  hbool. ,all(n:hnum. P(n))))
THM	not_suc	n:. n+1 = 0
THM	inv_suc	m,n:. m+1 = n+1    m = n
THM	induction	P:(). P(0) & (n:. P(n)  P(n+1))  (n:. P(n))

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