Def P  Q == P+Q

is mentioned by

Thm* R,R2:(TTProp). Thm* Trans(T)(R2(_1,_2)) Thm*  Thm* (x,y:T. (x R y)  (x R2 y))  (x,y:T. (x (R^*) y)  (x R2 y)  x = y)	[rel_star_closure]
Thm* n,m:, f:(nm), x1,x2:n, y1,y2:m. Thm* x1 = x2  y1 = y2 Thm*  Thm* (x:n, y:m. (x = x1 & y = y1)  (x = x2 & y = y2)  f(x,y) = 0) Thm*  Thm* sum(f(x,y) | x < n; y < m) = f(x1,y1)+f(x2,y2)	[pair_support_double_sum]
Thm* m:, P:(mProp). Thm* (i:m. Dec(P(i))) Thm*  Thm* (n,k:, f:(nm), g:(km). Thm* (increasing(f;n) Thm* (& increasing(g;k) Thm* (& (i:n. P(f(i))) Thm* (& (j:k. P(g(j))) Thm* (& (i:m. (j:n. i = f(j))  (j:k. i = g(j))))	[increasing_split]
Thm* m,n,k:, f:(nm), g:(km). Thm* increasing(f;n) Thm*  Thm* increasing(g;k) Thm*  Thm* (i:m. (j:n. i = f(j))  (j:k. i = g(j))) Thm*  Thm* (j1:n, j2:k. f(j1) = g(j2))  m = n+k	[disjoint_increasing_onto]
Def (R1  R2)(x,y) == (x R1 y)  (x R2 y)	[rel_or]

In prior sections: core bool 1 int 2 list 1 rel 1 sqequal 1

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