Def  x:A. B(x) == x:AB(x)

is mentioned by

Thm*  a,b:, e:({a..b}). ba  ( i:{a..b}. e(i)) = 0	[sum_via_intseg_null]
Thm*  a,b:, e:({a..b}). ba  ( i:{a..b}. e(i)) = 1	[mul_via_intseg_null]
Thm*  m,k:. mk  k!m = ((k!)  ((k-m)!))	[factorial_ratio2]
Thm*  m,k:. mk  k! = (k-m)!k!m	[factorial_ratio]
Thm*  k:. k!	[factorial_via_iter_wf]
Thm*  m,k:. 1  m  k  k!m = k(k-1)!(m-1)	[factorial_tail_via_iter_step_rw]
Thm*  m,k:. 1  m  k  (k',m':. k' = k-1  m' = m-1  k!m = kk'!m'  )	[factorial_tail_via_iter_step]
Thm*  m,k:. k<m  k!m = 0	[factorial_tail_via_iter_zero]
Thm*  m,k:. m = 0    k!m = 1	[factorial_tail_via_iter_null]
Thm*  n,m,k:. nk-m  mk  k!(n+m) = (k-m)!nk!m	[factorial_tail_split_mid]
Thm*  m,k:. k!m	[factorial_tail_via_iter_wf]
Thm*  (i:{a..b}. e(i) = 0)  ( i:{a..b}. e(i)) = 0	[zero_ann_iter_via_intseg]
Thm*  ( i:{a..b}. e(i)) = 0  (i:{a..b}. e(i) = 0)	[iter_prod_zero_iff_factor_zero]
Thm*  e:({a..b}). ( i:{a..b}. e(i)) = 1  (i:{a..b}. e(i) = 1)	[iter_nat_prod_one_iff_factors_one]
Thm*  a,b:, P:({a..b}Prop). (i:{a..b}. P(i))  (Or i:{a..b}. P(i))	[exist_intseg_vs_iter_or]
Thm*  a,b:, P:({a..b}Prop). ba  (i:{a..b}. P(i))	[exist_intseg_null]
Thm*  a,b:, P:({a..b}Prop). Thm*  a<b  ((i:{a..b}. P(i))  (i:{a..(b-1)}. P(i))  P(b-1))	[or_via_exist_intseg_split_last]
Thm*  a,b:, P:({a..b}Prop). Thm*  a<b Thm*   Thm*  (c:. b = c+1  ((i:{a..b}. P(i))  (i:{a..c}. P(i))  P(c)))	[or_via_exist_intseg_notnull]
Thm*  a,b:, P:({a..b}Prop). (i:{a..b}. P(i))  (And i:{a..b}. P(i))	[all_intseg_vs_iter_and]
Thm*  a,b:, P:({a..b}Prop). Thm*  a<b  ((i:{a..b}. P(i))  (i:{a..(b-1)}. P(i)) & P(b-1))	[and_via_all_intseg_split_last]
Thm*  a,b:, P:({a..b}Prop). Thm*  a<b Thm*   Thm*  (c:. b = c+1  ((i:{a..b}. P(i))  (i:{a..c}. P(i)) & P(c)))	[and_via_all_intseg_notnull]
Thm*  a,b:, e:({a..b}). Thm*  a<b  ( i:{a..b}. e(i)) = ( i:{a..b-1}. e(i))+e(b-1)	[sum_via_intseg_split_last]
Thm*  a,b,c:. (ab)c = acbc	[exp_reduce1]
Thm*  a,b:, f,g:({a..b}). Thm*  ( i:{a..b}. f(i))( i:{a..b}. g(i)) = ( i:{a..b}. f(i)g(i))	[mul_via_intseg_factors]
Thm*  a,b:, e:({a..b}). Thm*  a<b  ( i:{a..b}. e(i)) = ( i:{a..b-1}. e(i))e(b-1)	[mul_via_intseg_split_last]
Thm*  i:, x,y:. ixiy = i(x+y)	[sum_exponent]
Thm*  a,c,b:, e:({a..b}). Thm*  ac Thm*   Thm*  cb  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))( i:{c..b}. e(i))	[mul_via_intseg_split_mid]
Thm*  a,c,b:, e:({a..b}). Thm*  ac Thm*   Thm*  cb  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))+( i:{c..b}. e(i))	[sum_via_intseg_split_mid]
Thm*  a,b:, e:({a..b}), i:{a..b}. e(i) | ( i:{a..b}. e(i))	[components_divide_iter_mul]
Thm*  a,c,b:, e:({a..b}). Thm*  ac Thm*   Thm*  c<b Thm*   Thm*  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))e(c)( i:{c+1..b}. e(i))	[mul_via_intseg_split_pluck]
Thm*  a,c,b:, e:({a..b}). Thm*  ac Thm*   Thm*  c<b Thm*   Thm*  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))+e(c)+( i:{c+1..b}. e(i))	[sum_via_intseg_split_pluck]
Thm*  f:(AAA), u:A. Thm*  is_ident(A; f; u) Thm*   Thm*  is_assoc_sep(A; f) Thm*   Thm*  (a,c,b:, e:({a..b}A). Thm*  (ac Thm*  ( Thm*  (c<b Thm*  ( Thm*  ((Iter(f;u) i:{a..b}. e(i)) Thm*  (= Thm*  (f((Iter(f;u) i:{a..c}. e(i)),f(e(c),Iter(f;u) i:{c+1..b}. e(i))))	[iter_via_intseg_split_pluck]
Thm*  f:(AAA), u:A. Thm*  is_ident(A; f; u) Thm*   Thm*  is_assoc_sep(A; f) Thm*   Thm*  (a,b:, c:{a...b}, d:{c..b}, e:({a..b}A). Thm*  ((i:{a..b}. i<c  di  e(i) = u) Thm*  ( Thm*  ((Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) i:{c..d}. e(i)))	[iter_via_intseg_amputate_units]
Thm*  f:(AAA), u:A. Thm*  is_ident(A; f; u) Thm*   Thm*  is_assoc_sep(A; f) Thm*   Thm*  (a,c,b:, e:({a..b}A). Thm*  (ac Thm*  ( Thm*  (cb Thm*  ( Thm*  ((Iter(f;u) i:{a..b}. e(i)) Thm*  (= Thm*  (f((Iter(f;u) i:{a..c}. e(i)),Iter(f;u) i:{c..b}. e(i)))	[iter_via_intseg_split_mid]
Thm*  a,b:, f,g:({a..b}). Thm*  ( i:{a..b}. f(i))+( i:{a..b}. g(i)) = ( i:{a..b}. f(i)+g(i))	[add_via_intseg_addends]
Thm*  f:(AAA), u:A. Thm*  is_commutative_sep(A; f) Thm*   Thm*  is_ident(A; f; u) Thm*   Thm*  is_assoc_sep(A; f) Thm*   Thm*  (a,b:, e,g:({a..b}A). Thm*  (f((Iter(f;u) i:{a..b}. e(i)),Iter(f;u) i:{a..b}. g(i)) Thm*  (= Thm*  ((Iter(f;u) i:{a..b}. f(e(i),g(i))) Thm*  ( A)	[iter_via_intseg_comp_binop]
Thm*  f:(AAA), u:A, a,b,c,d:. Thm*  b-a = d-c Thm*   Thm*  (e:({a..b}A), g:({c..d}A). Thm*  ((i:{a..b}, j:{c..d}. j-i = c-a  e(i) = g(j)  A) Thm*  ( Thm*  ((Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) j:{c..d}. g(j)))	[iter_via_intseg_shift]
Thm*  f:(AAA), u:A, a,b:, e:({a..b}A), k:. Thm*  (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) j:{a+k..b+k}. e(j-k))	[iter_via_intseg_shift_rw]
Thm*  x:. 1x = 1	[one_exponentiation]
Thm*  a,b:, e:({a..b}). (i:{a..b}. e(i) = 1)  ( i:{a..b}. e(i)) = 1	[mul_via_intseg_one]
Thm*  f:(AAA), u:A. Thm*  is_ident(A; f; u) Thm*   Thm*  (a,b:, e:({a..b}A). Thm*  ((i:{a..b}. e(i) = u)  (Iter(f;u) i:{a..b}. e(i)) = u)	[iter_via_intseg_all_units]
Thm*  f:(AAA), u:A, a,b:, e:({a..b}A). Thm*  a<b Thm*   Thm*  (Iter(f;u) i:{a..b}. e(i)) = f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1))	[iter_via_intseg_split_last]
Thm*  a,b:, e:({a..b}). Thm*  a<b  (c:. b = c+1  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))+e(c))	[sum_via_intseg_notnull]
Thm*  a,b:, e:({a..b}). Thm*  a<b  (c:. b = c+1  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))e(c))	[mul_via_intseg_notnull]
Thm*  f:(AAA), u:A, a,b:, e:({a..b}A). Thm*  a<b Thm*   Thm*  (c:.  Thm*  (b = c+1 Thm*  ( Thm*  ((Iter(f;u) i:{a..b}. e(i)) = f((Iter(f;u) i:{a..c}. e(i)),e(c)))	[iter_via_intseg_notnull]
Thm*  a,b:, e:({a..b}). a+1 = b  ( i:{a..b}. e(i)) = e(a)	[mul_via_intseg_singleton]
Thm*  a,b:, e:({a..b}). a+1 = b  ( i:{a..b}. e(i)) = e(a)	[sum_via_intseg_singleton]
Thm*  f:(AAA), u:A. Thm*  is_ident(A; f; u) Thm*   Thm*  (a,b:, e:({a..b}A). a+1 = b  (Iter(f;u) i:{a..b}. e(i)) = e(a))	[iter_via_intseg_singleton]
Thm*  f:(AAA), u:A, a,b:, e:({a..b}A). Thm*  ba  (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) i:{a..a}. e(i))	[iter_via_intseg_nullnorm]
Thm*  f:(AAA), u:A, a,b:, e:({a..b}A). Thm*  ba  (Iter(f;u) i:{a..b}. e(i)) = u	[iter_via_intseg_null]
Thm*  x:. x1 = x	[exponent_one]
Thm*  x:. x0 = 1	[exponent_zero]
Thm*  f:(AAA), u:A, a,b:, e:({a..b}A). (Iter(f;u) i:{a..b}. e(i))  A	[iter_via_intseg_wf]
Thm*  P:(Prop).  Thm*  (a:, b:{...a}. P(a,b)) Thm*   Thm*  (a:, b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b))  (a,b:. P(a,b))	[all_int_segs_by_upper_ind]
Thm*  P:(Prop), a:. Thm*  (b:{...a}. P(a,b)) Thm*   Thm*  (b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b))  (b:. P(a,b))	[int_segs_from_base_by_upper_ind]
Thm*  P:(Prop), a:. Thm*  (b:{...a}. P(a,a)  P(a,b))  (b:{a...}. P(a,b))  (b:. P(a,b))	[split_int_domain_by_norm_lower]
Thm*  P:(Prop), a:. Thm*  (b:{a...}. (c:{a..b}. P(a,c))  P(a,b))  (b:{a...}. P(a,b))	[int_seg_upper_ind]
Thm*  P:(Prop).  Thm*  (a:, b:{...a}. P(a,b)) Thm*   Thm*  (a:. (b:{...a}. P(a,b))  (b:{a...}. P(a,b)))  (a,b:. P(a,b))	[all_int_pairs_via_all_splits]
Thm*  P:(Prop), a:. Thm*  (b:{...a}. P(a,b)) Thm*   Thm*  ((b:{...a}. P(a,b))  (b:{a...}. P(a,b)))  (b:. P(a,b))	[split_int_domain]
Thm*  f:(AAA). is_commutative_sep(A; f)  Prop	[is_commutative_sep_wf]
Thm*  f:(AAA). is_commutative(A; x,z.f(x,z))  Prop	[is_commutative_wf]
Thm*  f:(AAA). is_assoc_sep(A; f)  Prop	[is_assoc_sep_wf]
Thm*  f:(AAA), u,v:A. is_ident(A; f; u)  is_ident(A; f; v)  u = v	[binary_ident_unique]
Thm*  f:(AAA), u:A. is_ident(A; f; u)  Prop	[is_ident_wf]
Def  is_commutative(A; x,z.f(x;z)) == x,z:A. f(x;z) = f(z;x)  A	[is_commutative]
Def  is_assoc(A; x,z.f(x;z)) == x,y,z:A. f(x;f(y;z)) = f(f(x;y);z)  A	[is_assoc]
Def  is_ident(A; f; u) == x:A. f(u,x) = x & f(x,u) = x	[is_ident]

In prior sections: core well fnd int 1 bool 1 rel 1 quot 1 LogicSupplement int 2 union num thy 1 SimpleMulFacts

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