IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  Iter(f;u) i:{a..b}. e(i)
Def  == if a<b f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) else u fi
Def  (recursive)

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*  (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). (i:{a..b}. P(i))  (And i:{a..b}. P(i))[all_intseg_vs_iter_and]
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]
Def  k!m ==  i:{k-m..k}. i+1[factorial_tail_via_iter]

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

IteratedBinops Sections DiscrMathExt Doc