Selected Objects

THM	hcons_def	'a:S.  all (h:'a. all (h:'a. (t:hlist('a). equal (h:'a. (t:hlist('a). (cons(h,t) (h:'a. (t:hlist('a). ,abs_list (h:'a. (t:hlist('a). ,(pair (h:'a. (t:hlist('a). ,(((m:hnum. cond(equal(m,0),h,fst(rep_list(t),pre(m)))) (h:'a. (t:hlist('a). ,(,suc(snd(rep_list(t))))))))
THM	hnull_def	'a:S.  and(equal(null(nil),t),all(t:hlist('a). all(h:'a. equal(null(cons(h,t)),f))))
THM	hhd_wd	'a:S. all(t:hlist('a). all(h:'a. equal(hd(cons(h,t)),h)))
THM	htl_wd	'a:S. all(t:hlist('a). all(h:'a. equal(tl(cons(h,t)),t)))
THM	hit_sum_wd	and (equal(it_sum(nil),0) ,all(h:hnum. all(t:hlist(hnum). equal(it_sum(cons(h,t)),add(h,it_sum(t))))))
THM	happend_wd	'a:S.  and (all(l:hlist('a). equal(append(nil,l),l)) ,all ,(l1:hlist('a). all ,(l1:hlist('a). (l2:hlist('a). all ,(l1:hlist('a). (l2:hlist('a). (h:'a. equal ,(l1:hlist('a). (l2:hlist('a). (h:'a. (append(cons(h,l1),l2) ,(l1:hlist('a). (l2:hlist('a). (h:'a. ,cons(h,append(l1,l2)))))))
THM	hflat_wd	'a:S.  and (equal(flat(nil),nil) ,all ,(h:hlist('a). all ,(h:hlist('a). (t:hlist(hlist('a)). equal ,(h:hlist('a). (t:hlist(hlist('a)). (flat(cons(h,t)) ,(h:hlist('a). (t:hlist(hlist('a)). ,append(h,flat(t))))))
THM	hlength_wd	'a:S.  and (equal(length(nil),0) ,all(h:'a. all(t:hlist('a). equal(length(cons(h,t)),suc(length(t))))))
THM	hmap_wd	'a,'b:S. and (all(f:'a  'b. equal(map(f,nil),nil)) ,all ,(f:'a  'b. all ,(f:'a  'b. (h:'a. all ,(f:'a  'b. (h:'a. (t:hlist('a). equal ,(f:'a  'b. (h:'a. (t:hlist('a). (map(f,cons(h,t)) ,(f:'a  'b. (h:'a. (t:hlist('a). ,cons(f(h),map(f,t)))))))
THM	hmap2_wd	'a,'b,'c:S. and (all(f:'a  'b  'c. equal(map2(f,nil,nil),nil)) ,all ,(f:'a ,( 'b ,( 'c. all ,( 'c. (h1:'a. all ,( 'c. (h1:'a. (t1:hlist('a ,( 'c. (h1:'a. (t1:hlist(). all ,( 'c. (h1:'a. (t1:hlist(). (h2:'b. all ,( 'c. (h1:'a. (t1:hlist(). (h2:'b. (t2:hlist('b). equal ,( 'c. (h1:'a. (t1:hlist(). (h2:'b. (t2:hlist('b). (map2 ,( 'c. (h1:'a. (t1:hlist(). (h2:'b. (t2:hlist('b). ((f ,( 'c. (h1:'a. (t1:hlist(). (h2:'b. (t2:hlist('b). (,cons(h1,t1) ,( 'c. (h1:'a. (t1:hlist(). (h2:'b. (t2:hlist('b). (,cons(h2,t2)) ,( 'c. (h1:'a. (t1:hlist(). (h2:'b. (t2:hlist('b). ,cons ,( 'c. (h1:'a. (t1:hlist(). (h2:'b. (t2:hlist('b). ,(f(h1,h2) ,( 'c. (h1:'a. (t1:hlist(). (h2:'b. (t2:hlist('b). ,,map2(f,t1,t2)))))))))
THM	hel_wd	'a:S.  and (all(l:hlist('a). equal(el(0,l),hd(l))) ,all(l:hlist('a). all(n:hnum. equal(el(suc(n),l),el(n,tl(l))))))
THM	hevery_def	'a:S.  and (all(P:'a  hbool. equal(every(P,nil),t)) ,all ,(P:'a  hbool. all ,(P:'a  hbool. (h:'a. all ,(P:'a  hbool. (h:'a. (t:hlist('a). equal ,(P:'a  hbool. (h:'a. (t:hlist('a). (every(P,cons(h,t)) ,(P:'a  hbool. (h:'a. (t:hlist('a). ,and(P(h),every(P,t)))))))
THM	hlist_axiom	'b,'a:S. all (x:'b. all (x:'b. (f:'b (x:'b. ( 'a (x:'b. ( hlist('a) (x:'b. ( 'b. exists_unique (x:'b. ( 'b. (fn1:hlist('a)  'b. and (x:'b. ( 'b. (fn1:hlist('a)  'b. (equal(fn1(nil),x) (x:'b. ( 'b. (fn1:hlist('a)  'b. ,all (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. all (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). equal (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). (fn1(cons(h,t)) (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ,f (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ,(fn1(t) (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ,,h (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ,,t))))))))
THM	hnull_char	'a:S. and(null(nil),all(h:'a. all(t:hlist('a). not(null(cons(h,t))))))
THM	hlist_induct	'a:S.  all (P:hlist('a)  hbool. implies (P:hlist('a)  hbool. (and (P:hlist('a)  hbool. ((P(nil) (P:hlist('a)  hbool. (,all (P:hlist('a)  hbool. (,(t:hlist('a). implies (P:hlist('a)  hbool. (,(t:hlist('a). (P(t) (P:hlist('a)  hbool. (,(t:hlist('a). ,all(h:'a. P(cons(h,t)))))) (P:hlist('a)  hbool. ,all(l:hlist('a). P(l))))
THM	hlist_cases	'a:S.  all (l:hlist('a). or (l:hlist('a). (equal(l,nil) (l:hlist('a). ,exists(t:hlist('a). exists(h:'a. equal(l,cons(h,t))))))
THM	hcons_11	'a:S.  all (h:'a. all (h:'a. (t:hlist('a). all (h:'a. (t:hlist('a). (h':'a. all (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). equal (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). (equal(cons(h,t),cons(h',t')) (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). ,and (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). ,(equal(h,h') (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). ,,equal(t,t')))))))
THM	hnot_nil_cons	'a:S. all(t:hlist('a). all(h:'a. not(equal(nil,cons(h,t)))))
THM	hnot_cons_nil	'a:S. all(t:hlist('a). all(h:'a. not(equal(cons(h,t),nil))))
THM	hlist_not_eq	'a:S.  all (l1:hlist('a). all (l1:hlist('a). (l2:hlist('a). implies (l1:hlist('a). (l2:hlist('a). (not(equal(l1,l2)) (l1:hlist('a). (l2:hlist('a). ,all (l1:hlist('a). (l2:hlist('a). ,(h1:'a. all (l1:hlist('a). (l2:hlist('a). ,(h1:'a. (h2:'a. not (l1:hlist('a). (l2:hlist('a). ,(h1:'a. (h2:'a. (equal (l1:hlist('a). (l2:hlist('a). ,(h1:'a. (h2:'a. ((cons(h1,l1) (l1:hlist('a). (l2:hlist('a). ,(h1:'a. (h2:'a. (,cons(h2,l2))))))))
THM	hnot_eq_list	'a:S.  all (h1:'a. all (h1:'a. (h2:'a. implies (h1:'a. (h2:'a. (not(equal(h1,h2)) (h1:'a. (h2:'a. ,all (h1:'a. (h2:'a. ,(l1:hlist('a). all (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). not (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). (equal (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ((cons(h1,l1) (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). (,cons(h2,l2))))))))
THM	heq_list	'a:S.  all (h1:'a. all (h1:'a. (h2:'a. implies (h1:'a. (h2:'a. (equal(h1,h2) (h1:'a. (h2:'a. ,all (h1:'a. (h2:'a. ,(l1:hlist('a). all (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). implies (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). (equal(l1,l2) (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ,equal (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ,(cons(h1,l1) (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ,,cons(h2,l2))))))))
THM	hcons_char	'a:S. all(l:hlist('a). implies(not(null(l)),equal(cons(hd(l),tl(l)),l)))
THM	happend_assoc_2	'a:S.  all (l1:hlist('a). all (l1:hlist('a). (l2:hlist('a). all (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). equal (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). (append(l1,append(l2,l3)) (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). ,append(append(l1,l2),l3)))))
THM	hlength_append_2	'a:S.  all (l1:hlist('a). all (l1:hlist('a). (l2:hlist('a). equal (l1:hlist('a). (l2:hlist('a). (length(append(l1,l2)) (l1:hlist('a). (l2:hlist('a). ,add(length(l1),length(l2)))))
THM	hmap_append_2	'a,'b:S. all (f:'a  'b. all (f:'a  'b. (l1:hlist('a). all (f:'a  'b. (l1:hlist('a). (l2:hlist('a). equal (f:'a  'b. (l1:hlist('a). (l2:hlist('a). (map(f,append(l1,l2)) (f:'a  'b. (l1:hlist('a). (l2:hlist('a). ,append(map(f,l1),map(f,l2))))))
THM	hlength_map	'b,'a:S. all(l:hlist('a). all(f:'a  'b. equal(length(map(f,l)),length(l))))
THM	hevery_el	'a:S.  all (l:hlist('a). all (l:hlist('a). (P:'a  hbool. equal (l:hlist('a). (P:'a  hbool. (every(P,l) (l:hlist('a). (P:'a  hbool. ,all (l:hlist('a). (P:'a  hbool. ,(n:hnum. implies (l:hlist('a). (P:'a  hbool. ,(n:hnum. (lt(n,length(l)) (l:hlist('a). (P:'a  hbool. ,(n:hnum. ,P(el(n,l)))))))
THM	hevery_conj	'a:S.  all (Q:'a  hbool. all (Q:'a  hbool. (P:'a  hbool. all (Q:'a  hbool. (P:'a  hbool. (l:hlist('a). equal (Q:'a  hbool. (P:'a  hbool. (l:hlist('a). (every (Q:'a  hbool. (P:'a  hbool. (l:hlist('a). (((x:'a. and(P(x),Q(x))) (Q:'a  hbool. (P:'a  hbool. (l:hlist('a). (,l) (Q:'a  hbool. (P:'a  hbool. (l:hlist('a). ,and(every(P,l),every(Q,l))))))
THM	hlength_nil_2	'a:S. all(l:hlist('a). equal(equal(length(l),0),equal(l,nil)))
THM	hlength_cons_2	'a:S.  all (l:hlist('a). all (l:hlist('a). (n:hnum. equal (l:hlist('a). (n:hnum. (equal(length(l),suc(n)) (l:hlist('a). (n:hnum. ,exists (l:hlist('a). (n:hnum. ,(h:'a. exists (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). and (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). (equal(length(l'),n) (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). ,equal(l,cons(h,l'))))))))
THM	hlength_eq_cons	'a:S.  all (P:hlist('a) ( hbool. all ( hbool. (n:hnum. equal ( hbool. (n:hnum. (all(l:hlist('a). implies(equal(length(l),suc(n)),P(l))) ( hbool. (n:hnum. ,all ( hbool. (n:hnum. ,(l:hlist('a). implies ( hbool. (n:hnum. ,(l:hlist('a). (equal(length(l),n) ( hbool. (n:hnum. ,(l:hlist('a). ,(l:hlist('a). all(x:'a. P(cons(x,l)))) ( hbool. (n:hnum. ,(l:hlist('a). ,(l))))))
THM	hlength_eq_nil	'a:S.  all (P:hlist('a)  hbool. equal (P:hlist('a)  hbool. (all(l:hlist('a). implies(equal(length(l),0),P(l))) (P:hlist('a)  hbool. ,P(nil)))
THM	list_axiom	'b,'a:S, x:'b, f:('b'a('a List)'b). (fn1:(('a List)'b).  (fn1(nil) = x & (h:'a, t:'a List. fn1(cons(h; t)) = f(fn1(t),h,t))) & (fn1,y:(('a List)'b). & (fn1(nil) = x & (h:'a, t:'a List. fn1(cons(h; t)) = f(fn1(t),h,t)) & (& y(nil) = x & (& (h:'a, t:'a List. y(cons(h; t)) = f(y(t),h,t)) & ( & (fn1 = y)
THM	null_char	'a:S. True & (h:'a, t:'a List. True)
THM	list_induct	'a:S, P:(('a List)). P(nil) & (t:'a List. P(t)  (h:'a. P(cons(h; t))))  (l:'a List. P(l))
THM	list_cases	'a:S, l:'a List. l = nil  (t:'a List, h:'a. l = cons(h; t))
THM	cons_11	'a:S, h:'a, t:'a List, h':'a, t':'a List. cons(h; t) = cons(h'; t')  h = h' & t = t'
THM	not_nil_cons	'a:S, t:'a List, h:'a. nil = cons(h; t)
THM	not_nil_cons2	'a:S, t:'a List, h:'a. nil = cons(h; t)  False
THM	not_cons_nil	'a:S, t:'a List, h:'a. cons(h; t) = nil
THM	not_cons_nil2	'a:S, t:'a List, h:'a. cons(h; t) = nil  False
THM	list_not_eq	'a:S, l1,l2:'a List. l1 = l2  (h1,h2:'a. cons(h1; l1) = cons(h2; l2))
THM	not_eq_list	'a:S, h1,h2:'a. h1 = h2  (l1,l2:'a List. cons(h1; l1) = cons(h2; l2))
THM	eq_list	'a:S, h1,h2:'a. h1 = h2  (l1,l2:'a List. l1 = l2  cons(h1; l1) = cons(h2; l2))
THM	cons_char	'a:S, l:'a List. mt(l)  cons(head(l); tl(l)) = l
THM	append_assoc_2	'a:S, l1,l2,l3:'a List. (l1 @ (l2 @ l3)) = ((l1 @ l2) @ l3)
THM	length_append_2	'a:S, l1,l2:'a List. ||l1 @ l2|| = ||l1||+||l2||
THM	map_append_2	'a,'b:S, f:('a'b), l1,l2:'a List. map(f;l1 @ l2) = (map(f;l1) @ map(f;l2))
THM	length_map	'b,'a:S, l:'a List, f:('a'b). ||map(f;l)|| = ||l||
THM	every_el	'a:S, l:'a List, P:('a). every(P;l)  (n:. n<||l||  P(l[n]))
THM	every_conj_2	'a:S, Q,P:('a), l:'a List. every(x:'a. (P(x))(Q(x));l) = (every(P;l)every(Q;l))
THM	every_conj	'a:S, Q,P:('a), l:'a List. every(x:'a. (P(x))(Q(x));l)  every(P;l) & every(Q;l)
THM	length_nil_2	'a:S, l:'a List. ||l|| = 0    l = nil
THM	length_cons_2	'a:S, l:'a List, n:. ||l|| = n+1    (h:'a, l':'a List. ||l'|| = n   & l = cons(h; l'))
THM	length_eq_cons	'a:S, P:(('a List)), n:. (l:'a List. ||l|| = n+1    P(l)) (l:'a List. ||l|| = n    (x:'a. P(cons(x; l))))
THM	length_eq_nil	'a:S, P:(('a List)). (l:'a List. ||l|| = 0    P(l))  P(nil)
THM	cons_11_2	'a:S, h:'a, t:'a List, h':'a, t':'a List. cons(h; t) = cons(h'; t')  h = h' & t = t'

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