Def P  Q == PQ

is mentioned by

Thm* a:Id, l:IdLnk, tg:Id. locl(a) = rcv(l; tg)  False	[not_locl_rcv]
Thm* a:Id, l:IdLnk, tg:Id. rcv(l; tg) = locl(a)  False	[not_rcv_locl]
Thm* a,b:Id. locl(a) = locl(b)  a = b	[locl_one_one]
Thm* f:((T List)), t,t':. Thm* t<t'  concat(map(f;upto(t))) @ (f(t))  concat(map(f;upto(t')))	[concat_map_upto]
Thm* ll1,ll2:(T List) List. ll1  ll2  concat(ll1)  concat(ll2)	[concat_iseg]
Thm* L:Top List, n:. ||L||n  (firstn(n;L) ~ L)	[firstn_all]
Thm* t',m:, T:Type, f:(T), P:(T). Thm* m+1||filter(P;map(f;upto(t')))|| Thm*  Thm* (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )	[filter_map_upto2]
Thm* i,j:. Thm* i<j Thm*  Thm* (f:(T), P:(T). Thm* (P(f(i))  ||filter(P;map(f;upto(i)))||<||filter(P;map(f;upto(j)))||)	[filter_map_upto]
Thm* P:(TProp), A,B:T List. Thm* A = B  (i:||A||. P(A[i]))  A = B  {x:T| P(x) } List	[list-eq-set-type]
Thm* n,i:. i<n  (i  upto(n))	[member_upto2]
Thm* i,j:. ij  upto(i)  upto(j)	[upto_iseg]
Thm* f:(). (n:. f(n))  f(mu(f)) & (i:. i<mu(f)  f(i))	[mu-property]
Thm* f:(). (n:. f(n))  mu(f)	[mu_wf]
Thm* P:(TProp).  Thm* (x:T. Dec(P(x))) Thm*  Thm* (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L)))	[finite-decidable-set]
Thm* P:(TProp).  Thm* (x:T. SqStable(P(x))) Thm*  Thm* (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L)))	[finite-set-type]
Thm* x:A, y:B. inl(x) = inr(y)  A+B  False	[inl_eq_inr]
Thm* L:T List, P:(TProp). (xL.P(x))  L  {x:T| P(x) } List	[list-set-type2]
Thm* L:A List, x:A. (A r B)  (x  L)  (x  L)	[l_member_subtype]
Thm* f:(A), L:A List. 0<||L||  (aL.(xL.f(x)f(a)))	[maximal-in-list]
Thm* strong-subtype(A;B)  (L:A List, x:B. (x  L)  (x  L))	[strong-subtype-l_member]
Thm* strong-subtype(A;B)  (L:A List, x:B. (x  L)  x  A)	[strong-subtype-l_member-type]
Thm* P:(AProp). strong-subtype(A;B)  strong-subtype({x:A| P(x) };B)	[strong-subtype-set3]
Thm* strong-subtype(A;B) Thm*  Thm* (P:(AProp), Q:(BProp). Thm* ((x:A. P(x)  Q(x))  strong-subtype({x:A| P(x) };{x:B| Q(x) }))	[strong-subtype-set]
Thm* strong-subtype(A;B)  strong-subtype(B;C)  strong-subtype(A;C)	[strong-subtype_transitivity]
Thm* (A r B)  (B r C)  (A r C)	[subtype_rel_transitivity]
Thm* (A r B)  ((A List) r (B List))	[subtype_rel_list]
Thm* B:(AType), C:Type, D:(CType). Thm* (A r C)  (a:A. B(a) r D(a))  ((a:AB(a)) r (c:CD(c)))	[subtype_rel_product]
Thm* B:(AType), C:Type, D:(CType). Thm* (C r A)  (a:C. B(a) r D(a))  ((a:AB(a)) r (c:CD(c)))	[subtype_rel_dep_function]
Thm* (C r A)  (B r D)  ((AB) r (CD))	[subtype_rel_function]
Thm* x,y:A. (A r B)  x = y  x = y  B	[equal_functionality_wrt_subtype_rel]
Def strong-subtype(A;B) Def == (A r B) Def == & ({b:B| a:A. b = a  B } r A) Def == & (a1,a2:A. a1 = a2  B  a1 = a2)	[strong-subtype]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 sqequal 1 union mb basic rel 1 mb nat mb list 1 num thy 1 mb list 2

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html