Selected Objects

THM	equal_functionality_wrt_subtype_rel	x,y:A. (A r B)  x = y  x = y  B
THM	subtype_rel_function	(C r A)  (B r D)  ((AB) r (CD))
THM	subtype_rel_dep_function	B:(AType), C:Type, D:(CType). (C r A)  (a:C. B(a) r D(a))  ((a:AB(a)) r (c:CD(c)))
THM	subtype_rel_product	B:(AType), C:Type, D:(CType). (A r C)  (a:A. B(a) r D(a))  ((a:AB(a)) r (c:CD(c)))
THM	subtype_rel_list	(A r B)  ((A List) r (B List))
THM	subtype_rel_transitivity	(A r B)  (B r C)  (A r C)
def	strong-subtype	strong-subtype(A;B) == (A r B) == & ({b:B| a:A. b = a  B } r A) == & (a1,a2:A. a1 = a2  B  a1 = a2)
THM	strong-subtype-self	strong-subtype(A;A)
THM	strong-subtype_transitivity	strong-subtype(A;B)  strong-subtype(B;C)  strong-subtype(A;C)
THM	subtype_rel_self	A r A
THM	strong-subtype-set	strong-subtype(A;B) (P:(AProp), Q:(BProp). ((x:A. P(x)  Q(x))  strong-subtype({x:A| P(x) };{x:B| Q(x) }))
THM	strong-subtype-set2	P:(AProp). strong-subtype({x:A| P(x) };A)
THM	strong-subtype-set3	P:(AProp). strong-subtype(A;B)  strong-subtype({x:A| P(x) };B)
THM	strong-subtype-l_member-type	strong-subtype(A;B)  (L:A List, x:B. (x  L)  x  A)
THM	strong-subtype-l_member	strong-subtype(A;B)  (L:A List, x:B. (x  L)  (x  L))
THM	sq_stable__subtype_rel	SqStable(A r B)
THM	fun_exp_add_sq	n,m:, f,i:Top. (f^n+m(i)) ~ (f^n(f^m(i)))
THM	maximal-in-list	f:(A), L:A List. 0<||L||  (aL.(xL.f(x)f(a)))
THM	l_member_subtype	L:A List, x:A. (A r B)  (x  L)  (x  L)
def	l_interval	l_interval(l;j;i) == mklist(i-j;x.l[(j+x)])
THM	length_l_interval	l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j
THM	select_l_interval	l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)]
THM	hd_l_interval	l:T List, i:||l||, j:i. hd(l_interval(l;j;i)) = l[j]
THM	last_l_interval	l:T List, i:||l||, j:i. last(l_interval(l;j;i)) = l[(i-1)]
def	pairwise	(x,yL.P(x;y)) == i:||L||, j:i. P(L[j];L[i])
THM	pairwise-cons	T:Type{i}, x:T, L:T List, P:(TTProp{i'}). (x,y[x / L].P(x,y))  (x,yL.P(x,y)) & (yL.P(x,y))
THM	list-set-type	L:T List. L  {x:T| (x  L) } List
THM	list-set-type2	L:T List, P:(TProp). (xL.P(x))  L  {x:T| P(x) } List
THM	append_assoc_sq	as,bs,cs:Top List. ((as @ bs) @ cs) ~ (as @ bs @ cs)
THM	inl_eq_inr	x:A, y:B. inl(x) = inr(y)  A+B  False
def	finite-type	finite-type(T) == n:, f:(nT). Surj(n; T; f)
THM	finite-type-iff-list	finite-type(T)  (L:T List. x:T. (x  L))
THM	finite-set-type	P:(TProp).  (x:T. SqStable(P(x))) (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L)))
THM	finite-decidable-set	P:(TProp).  (x:T. Dec(P(x))) (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L)))
THM	map-map	as:Top List, f,g:Top. map(g;map(f;as)) ~ map(g o f;as)
THM	map_is_nil	f:(AB), l:A List. map(f;l) = nil  l = nil
THM	map-id	L:Top List. map(x.x;L) ~ L
THM	length-map	f:Top, T:Type, L:T List. ||map(f;L)|| ~ ||L||
THM	select-map	f:Top, T:Type, L:T List, i:||L||. map(f;L)[i] ~ (f(L[i]))
THM	general_length_nth_tl	r:, L:Top List. ||nth_tl(r;L)|| = if r<||L|| ||L||-r else 0 fi
def	mu	mu(f) == if f(0) 0 else mu(x.f(x+1))+1 fi  (recursive)
THM	mu-property	f:(). (n:. f(n))  f(mu(f)) & (i:. i<mu(f)  f(i))
def	upto	upto(n) == if n=0 nil else upto(n-1) @ [(n-1)] fi  (recursive)
THM	length_upto	n:. ||upto(n)|| ~ n
THM	upto_decomp	m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))
THM	upto_iseg	i,j:. ij  upto(i)  upto(j)
THM	select_upto	m:, n:m. upto(m)[n] = n
THM	member_upto	n,i:. (i  upto(n))  i<n
THM	member_upto2	n,i:. i<n  (i  upto(n))
THM	before-upto	n:, x,y:n. x before y  upto(n)  x<y
THM	list-eq-set-type	P:(TProp), A,B:T List. A = B  (i:||A||. P(A[i]))  A = B  {x:T| P(x) } List
THM	before-map	f:(TT'), L:T List, x',y':T'. x' before y'  map(f;L)  (x,y:T. x before y  L & f(x) = x' & f(y) = y')
THM	filter_append_sq	P:(T), A:T List, B:Top. filter(P;A @ B) ~ (filter(P;A) @ filter(P;B))
THM	filter_map_upto	i,j:. i<j (f:(T), P:(T). (P(f(i))  ||filter(P;map(f;upto(i)))||<||filter(P;map(f;upto(j)))||)
THM	filter_map_upto2	t',m:, T:Type, f:(T), P:(T). m+1||filter(P;map(f;upto(t')))|| (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )
THM	first0	L:Top List. firstn(0;L) ~ nil
THM	firstn_append	L1,L2:Top List, n:(||L1||+1). firstn(n;L1 @ L2) ~ firstn(n;L1)
THM	firstn_all	L:Top List, n:. ||L||n  (firstn(n;L) ~ L)
THM	firstn_map	f:(TopTop), n:, l:Top List. firstn(n;map(f;l)) ~ map(f;firstn(n;l))
THM	firstn_upto	n,m:. firstn(n;upto(m)) ~ if nm upto(n) else upto(m) fi
def	concat	concat(ll) == reduce(l,l'. l @ l';nil;ll)
THM	concat_append	ll1,ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2))
THM	concat-cons	l:Top List, ll:(Top List) List. concat([l / ll]) ~ (l @ concat(ll))
THM	select_concat	ll:(T List) List, n:||concat(ll)||. m:||ll||.  ||concat(firstn(m;ll))||n & n-||concat(firstn(m;ll))||<||ll[m]|| & concat(ll)[n] = ll[m][(n-||concat(firstn(m;ll))||)]
THM	member-concat	ll:(T List) List, x:T. (x  concat(ll))  (l:T List. (l  ll) & (x  l))
THM	l_member_decomp	l:T List, x:T. (x  l)  (l1,l2:T List. l = (l1 @ [x] @ l2))
THM	concat_iseg	ll1,ll2:(T List) List. ll1  ll2  concat(ll1)  concat(ll2)
THM	concat_map_upto	f:((T List)), t,t':. t<t'  concat(map(f;upto(t))) @ (f(t))  concat(map(f;upto(t')))
def	Id	Id == Atom
THM	Id_sq	SQType(Id)
def	mkid	x_n == <x,n>
def	IdLnk	IdLnk == IdId
THM	IdLnk_sq	SQType(IdLnk)
def	lnk-inv	lnk-inv(l) == <1of(2of(l)),1of(l),2of(2of(l))>
THM	lnk-inv-inv	l:IdLnk. lnk-inv(lnk-inv(l)) = l  IdLnk
def	Msg	Msg(M) == l:IdLnkt:IdM(l,t)
COM	msg	msg(l;t;v) == <l,t,v>
def	mlnk	mlnk(m) == 1of(m)
def	mtag	mtag(m) == 1of(2of(m))
def	haslink	haslink(l; m) == mlnk(m) = l
def	Msg_sub	Msg_sub(l; M) == {m:Msg(M)| haslink(l; m) }
def	Knd	Knd == (IdLnkId)+Id
THM	Knd_sq	SQType(Knd)
def	isrcv	isrcv(k) == isl(k)
def	islocal	islocal(k) == isl(k)
THM	islocal-not-isrcv	k:Knd. islocal(k) ~ isrcv(k)
def	rcv	rcv(l; tg) == inl(<l,tg>)
def	locl	locl(a) == inr(a)
THM	locl_one_one	a,b:Id. locl(a) = locl(b)  a = b
THM	not_rcv_locl	a:Id, l:IdLnk, tg:Id. rcv(l; tg) = locl(a)  False
THM	not_locl_rcv	a:Id, l:IdLnk, tg:Id. locl(a) = rcv(l; tg)  False

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