Selected Objects

THM	append_firstn_lastn	L:T List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) = L
THM	append_split2	L:T List, P:(||L||Prop). (x:||L||. Dec(P(x))) (i,j:||L||. P(i)  i<j  P(j)) (L_1,L_2:T List. L = (L_1 @ L_2) & (i:||L||. P(i)  ||L_1||i))
THM	non_nil_length	L:T List. L = nil  0<||L||
THM	length_zero	l:T List. ||l|| = 0    l = nil
THM	list_decomp	L:T List. 0<||L||  (L ~ [hd(L) / tl(L)])
THM	nth_tl_decomp	m:, L:T List. m<||L||  (nth_tl(m;L) ~ [L[m] / nth_tl(1+m;L)])
THM	map_append_sq	f,as':Top, A:Type, as:A List. map(f;as @ as') ~ (map(f;as) @ map(f;as'))
THM	list_extensionality	a,b:T List. ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b
THM	map_equal	a:T List, f,g:(TT'). (i:. i<||a||  f(a[i]) = g(a[i]))  map(f;a) = map(g;a)
THM	list_decomp_reverse	L:T List. 0<||L||  (x:T, L':T List. L = (L' @ [x]))
THM	list_append_singleton_ind	Q:((T List)Prop).  Q(nil)  (ys:T List, x:T. Q(ys)  Q(ys @ [x]))  (zs:T List. Q(zs))
THM	cons_one_one	a,a':T, b,b':T List. [a / b] = [a' / b']  a = a' & b = b'
THM	map_length_nat	f:(AB), as:A List. ||map(f;as)|| = ||as||
THM	list_2_decomp	z:T List. ||z|| = 2    z = [z[0]; z[1]]
THM	append_is_nil	l1,l2:T List. (l1 @ l2) = nil  l1 = nil & l2 = nil
THM	append_nil_sq	l:T List. (l @ nil) ~ l
def	mklist	mklist(n;f) == primrec(n;nil;i,l. l @ [(f(i))])
THM	mklist_length	n:, f:(nT). ||mklist(n;f)|| = n
THM	mklist_select	n:, f:(nT), i:n. mklist(n;f)[i] = f(i)
def	l_member	(x  l) == i:. i<||l|| & x = l[i]  T
THM	member_exists	L:T List. L = nil  (x:T. (x  L))
THM	map_equal2	a:T List, f,g:(TT'). (x:T. (x  a)  f(x) = g(x))  map(f;a) = map(g;a)
THM	trivial_map	a:T List, f:(TT). (x:T. (x  a)  f(x) = x)  map(f;a) = a
THM	member_tl	as:T List, x:T. 0<||as||  (x  tl(as))  (x  as)
THM	nil_member	x:T. (x  nil)  False
THM	null_member	L:T List, x:T. null(L)  (x  L)
THM	member_null	L:T List, x:T. (x  L)  null(L)
THM	cons_member	l:T List, a,x:T. (x  [a / l])  x = a  (x  l)
THM	l_member_decidable	x:T, l:T List. (y:T. Dec(x = y))  Dec((x  l))
THM	member_append	x:T, l1,l2:T List. (x  l1 @ l2)  (x  l1)  (x  l2)
THM	select_member	L:T List, i:||L||. (L[i]  L)
THM	member_singleton	a,x:T. (x  [a])  x = a
THM	member_map	a:T List, x:T', f:(TT'). (x  map(f;a))  (y:T. (y  a) & x = f(y))
def	last	last(L) == L[(||L||-1)]
THM	last_cons	L:T List, x:T. null(L)  last([x / L]) = last(L)
def	sublist	L1  L2 == f:(||L1||||L2||).  == increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))]  T)
THM	sublist_transitivity	L1,L2,L3:T List. L1  L2  L2  L3  L1  L3
THM	length_sublist	L1,L2:T List. L1  L2  ||L1||||L2||
THM	cons_sublist_nil	x:T, L:T List. [x / L]  nil  False
THM	proper_sublist_length	L1,L2:T List. L1  L2  ||L1|| = ||L2||    L1 = L2
THM	sublist_antisymmetry	L1,L2:T List. L1  L2  L2  L1  L1 = L2
THM	nil_sublist	L:T List. nil  L  True
THM	cons_sublist_cons	x1,x2:T, L1,L2:T List. [x1 / L1]  [x2 / L2]  x1 = x2 & L1  L2  [x1 / L1]  L2
THM	sublist_weakening	L1,L2:T List. L1 = L2  L1  L2
THM	sublist_nil	L:T List. L  nil  L = nil
THM	sublist_tl	L1,L2:T List. null(L2)  L1  tl(L2)  L1  L2
THM	sublist_pair	L:T List, i,j:||L||. i<j  [L[i]; L[j]]  L
THM	member_iff_sublist	x:T, L:T List. (x  L)  [x]  L
def	l_before	x before y  l == [x; y]  l
THM	l_tricotomy	x,y:T, L:T List. (x  L)  (y  L)  x = y  x before y  L  y before x  L
THM	l_before_member	L:T List, a,b:T. a before b  L  (b  L)
THM	nil_before	x,y:T. x before y  nil  False
THM	l_before_member2	L:T List, a,b:T. a before b  L  (a  L)
THM	cons_before	l:T List, a,x,y:T. x before y  [a / l]  x = a & (y  l)  x before y  l
def	listp	A List == {l:(A List)| (0<||l||) }
THM	listp_properties	l:A List. ||l||1
def	filter	filter(P;l) == reduce(a,v. if P(a) [a / v] else v fi;nil;l)
THM	member_filter	P:(T), L:T List, x:T. (x  filter(P;L))  (x  L) & P(x)
THM	filter_functionality	L:A List, f1,f2:(A). f1 = f2  (filter(f1;L) ~ filter(f2;L))
THM	filter_append	P:(T), l1,l2:T List. filter(P;l1 @ l2) ~ (filter(P;l1) @ filter(P;l2))
THM	filter_filter	P1,P2:(T), L:T List. filter(P1;filter(P2;L)) ~ filter(t.(P1(t))(P2(t));L)
THM	filter_type	P:(T), l:T List. filter(P;l)  {x:T| P(x) } List
THM	filter_map	f:(T1T2), Q:(T2), L:T1 List. filter(Q;map(f;L)) = map(f;filter(Q o f;L))
def	iseg	l1  l2 == l:T List. l2 = (l1 @ l)
THM	cons_iseg	a,b:T, l1,l2:T List. [a / l1]  [b / l2]  a = b & l1  l2
THM	iseg_transitivity	l1,l2,l3:T List. l1  l2  l2  l3  l1  l3
THM	iseg_append	l1,l2,l3:T List. l1  l2  l1  l2 @ l3
THM	firstn_is_iseg	L1,L2:T List. L1  L2  (n:(||L2||+1). L1 = firstn(n;L2))
THM	iseg_transitivity2	l1,l2,l3:T List. l2  l3  l1  l2  l1  l3
THM	iseg_weakening	l:T List. l  l
THM	nil_iseg	l:T List. nil  l
THM	iseg_select	l1,l2:T List. l1  l2  ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i])
THM	iseg_member	l1,l2:T List, x:T. l1  l2  (x  l1)  (x  l2)
THM	iseg_nil	L:T List. L  nil  null(L)
THM	filter_iseg	P:(T), L2,L1:T List. L1  L2  filter(P;L1)  filter(P;L2)
THM	iseg_length	l1,l2:T List. l1  l2  ||l1||||l2||
THM	iseg_is_sublist	L_1,L_2:T List. L_1  L_2  L_1  L_2
def	list_accum	list_accum(x,a.f(x;a);y;l) == Case of l; nil  y ; b.l'  list_accum(x,a.f(x;a);f(y;b);l') (recursive)
def	zip	zip(as;bs) == Case of as == Canil  nil == Caa.as'  Case of bs; nil  nil ; b.bs'  [<a,b> / zip(as';bs')] (recursive)
THM	zip_length	as:T1 List, bs:T2 List. ||zip(as;bs)||||as|| & ||zip(as;bs)||||bs||
THM	select_zip	as:T1 List, bs:T2 List, i:. i<||zip(as;bs)||  zip(as;bs)[i] = <as[i],bs[i]>
THM	length_zip	as:T1 List, bs:T2 List. ||as|| = ||bs||    ||zip(as;bs)|| = ||as||
def	unzip	unzip(as) == <map(p.1of(p);as),map(p.2of(p);as)>
THM	unzip_zip	as:T1 List, bs:T2 List. ||as|| = ||bs||    unzip(zip(as;bs)) = <as,bs>
THM	zip_unzip	as:(T1T2) List. zip(1of(unzip(as));2of(unzip(as))) = as
def	find	(first x  as s.t. P(x) else d) == Case of filter(x.P(x);as); nil  d ; a.b  a
THM	find_property	P:(T), as:T List, d:T. ((first a  as s.t. P(a) else d)  as)  (first a  as s.t. P(a) else d) = d
def	no_repeats	no_repeats(T;l) == i,j:. i<||l||  j<||l||  i = j  l[i] = l[j]  T
THM	no_repeats_iff	l:T List. no_repeats(T;l)  (x,y:T. x before y  l  x = y)
THM	no_repeats_cons	l:T List, x:T. no_repeats(T;[x / l])  no_repeats(T;l) & (x  l)
THM	append_overlapping_sublists	L1,L2,L:T List, x:T. no_repeats(T;L)  L1 @ [x]  L  [x / L2]  L  L1 @ [x / L2]  L
THM	l_before_transitivity	l:T List, x,y,z:T. no_repeats(T;l)  x before y  l  y before z  l  x before z  l
THM	no_repeats_nil	no_repeats(T;nil)

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