IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
IteratedBinops
Nuprl Section: IteratedBinops - Iterated Binary Operations

Selected Objects
IntroductionIntroductory Remarks
defis_ident
(u is an identity element for operation f on A)
is_ident(Afu) == x:Af(u,x) = x & f(x,u) = x
THMbinary_ident_unique
A binary operation has at most one identity value.
f:(AAA), u,v:A. is_ident(Afu is_ident(Afv u = v
THMintmul_ident_one
is_ident(; (x,yxy); 1)
THMnatmul_ident_one
is_ident(; (x,yxy); 1)
is_ident(; (x,yx+y); 0)
is_ident(; (x,yx+y); 0)
defis_assoc
Associativity of a function
is_assoc(Ax,z.f(x;z)) == x,y,z:Af(x;f(y;z)) = f(f(x;y);z A
defis_assoc_sep
Associativity of a function
is_assoc_sep(Af) == is_assoc(Ax,y.(f(x,y)))
THMis_assoc_intmul
is_assoc_sep(; (x,yxy))
is_assoc_sep(; (x,yx+y))
defis_commutative
Commutativity of a function
is_commutative(Ax,z.f(x;z)) == x,z:Af(x;z) = f(z;x A
defis_commutative_sep
Commutativity of a function
is_commutative_sep(Af) == is_commutative(Ax,z.(f(x,z)))
THMis_commutative_sep_intmul
is_commutative_sep(; (x,yxy))
is_commutative_sep(; (x,yx+y))
THMsplit_int_domain
P:(Prop), a:.
(b:{...a}. P(a,b))

((b:{...a}. P(a,b))  (b:{a...}. P(a,b)))  (b:P(a,b))
THMall_int_pairs_via_all_splits
P:(Prop).
(a:b:{...a}. P(a,b))

(a:. (b:{...a}. P(a,b))  (b:{a...}. P(a,b)))  (a,b:P(a,b))
THMint_seg_upper_ind
P:(Prop), a:.
(b:{a...}. (c:{a..b}. P(a,c))  P(a,b))  (b:{a...}. P(a,b))
THMsplit_int_domain_by_norm_lower
P:(Prop), a:.
(b:{...a}. P(a,a P(a,b))  (b:{a...}. P(a,b))  (b:P(a,b))
THMint_segs_from_base_by_upper_ind
P:(Prop), a:.
(b:{...a}. P(a,b))

(b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b))  (b:P(a,b))
THMall_int_segs_by_upper_ind
P:(Prop).
(a:b:{...a}. P(a,b))

(a:b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b))  (a,b:P(a,b))
defiter_via_intseg
Iteration of a binary operator over a finite sequence of values. Some special cases of this iteration operator include sum, product and exponentiation:

 i:{a..b}. e(i) Iter(x,y. x+y;0) i:{a..b}. e(i) i:b. e(i) Iter(x,y. x+y;0) i:{0..b}. e(i) i:{a..b}. e(i) Iter(x,y. xy;1) i:{a..b}. e(i) i:b. e(i) Iter(x,y. xy;1) i:{0..b}. e(i) eb Iter(x,y. xy;1) :{0..b}. e Or i:{a..b}. e(i) Iter(x,y. x  y;False) i:{a..b}. e(i) Or i:b. e(i) Iter(x,y. x  y;False) i:{0..b}. e(i) And i:{a..b}. e(i) Iter(x,y. x & y;True) i:{a..b}. e(i) And i:b. e(i) Iter(x,y. x & y;True) i:{0..b}. e(i)

Iter(f;ui:{a..b}. e(i)
== if a<b f((Iter(f;ui:{a..b-1}. e(i)),e(b-1)) else u fi
(recursive)
THMexponent_zero
x:x0 = 1
THMexponent_one
x:x1 = x
THMiter_via_intseg_null
Iteration over a null sequence is the identity element.
f:(AAA), u:Aa,b:e:({a..b}A). ba  (Iter(f;ui:{a..b}. e(i)) = u
THMiter_via_intseg_nullnorm
f:(AAA), u:Aa,b:e:({a..b}A).
ba  (Iter(f;ui:{a..b}. e(i)) = (Iter(f;ui:{a..a}. e(i))
THMiter_via_intseg_singleton
Iteration over a singleton is just the value for the one index.
f:(AAA), u:A.
is_ident(Afu)

(a,b:e:({a..b}A). a+1 = b  (Iter(f;ui:{a..b}. e(i)) = e(a))
THMsum_via_intseg_singleton
a,b:e:({a..b}). a+1 = b  ( i:{a..b}. e(i)) = e(a)
THMmul_via_intseg_singleton
a,b:e:({a..b}). a+1 = b  ( i:{a..b}. e(i)) = e(a)
THMiter_via_intseg_notnull
Splitting the last element from the range of iteration.
f:(AAA), u:Aa,b:e:({a..b}A).
a<b

(c:
(b = c+1  (Iter(f;ui:{a..b}. e(i)) = f((Iter(f;ui:{a..c}. e(i)),e(c)))
THMmul_via_intseg_notnull
a,b:e:({a..b}).
a<b  (c:b = c+1  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))e(c))
THMsum_via_intseg_notnull
a,b:e:({a..b}).
a<b  (c:b = c+1  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))+e(c))
THMiter_via_intseg_split_last
Splitting the last element from the domain of iteration.
f:(AAA), u:Aa,b:e:({a..b}A).
a<b  (Iter(f;ui:{a..b}. e(i)) = f((Iter(f;ui:{a..b-1}. e(i)),e(b-1))
THMiter_via_intseg_all_units
Iterating over only identity values gives the identity value itself.
f:(AAA), u:A.
is_ident(Afu)

(a,b:e:({a..b}A).
((i:{a..b}. e(i) = u (Iter(f;ui:{a..b}. e(i)) = u)
THMmul_via_intseg_one
a,b:e:({a..b}). (i:{a..b}. e(i) = 1)  ( i:{a..b}. e(i)) = 1
THMone_exponentiation
x:. 1x = 1
THMiter_via_intseg_shift_rw
Shifting the range of iteration.
f:(AAA), u:Aa,b:e:({a..b}A), k:.
(Iter(f;ui:{a..b}. e(i)) = (Iter(f;uj:{a+k..b+k}. e(j-k))
THMiter_via_intseg_shift
Shifting the range of iteration.
f:(AAA), u:Aa,b,c,d:.
b-a = d-c

(e:({a..b}A), g:({c..d}A).
((i:{a..b}, j:{c..d}. j-i = c-a  e(i) = g(j A)
(
((Iter(f;ui:{a..b}. e(i)) = (Iter(f;uj:{c..d}. g(j)))
THMiter_via_intseg_comp_binop
Joining two iterations pairwise.
f:(AAA), u:A.
is_commutative_sep(Af)

is_ident(Afu)

is_assoc_sep(Af)

(a,b:e,g:({a..b}A).
(f((Iter(f;ui:{a..b}. e(i)),Iter(f;ui:{a..b}. g(i))
(=
((Iter(f;ui:{a..b}. f(e(i),g(i)))
( A)
a,b:f,g:({a..b}).
( i:{a..b}. f(i))+( i:{a..b}. g(i)) = ( i:{a..b}. f(i)+g(i))
THMiter_via_intseg_split_mid
Splitting the range of iteration.
f:(AAA), u:A.
is_ident(Afu)

is_assoc_sep(Af)

(a,c,b:e:({a..b}A).
(ac
(
(cb
(
((Iter(f;ui:{a..b}. e(i))
(=
(f((Iter(f;ui:{a..c}. e(i)),Iter(f;ui:{c..b}. e(i)))
THMiter_via_intseg_amputate_units
Removing units from the ends of the range of iteration preserves the result.
f:(AAA), u:A.
is_ident(Afu)

is_assoc_sep(Af)

(a,b:c:{a...b}, d:{c..b}, e:({a..b}A).
((i:{a..b}. i<c  di  e(i) = u)
(
((Iter(f;ui:{a..b}. e(i)) = (Iter(f;ui:{c..d}. e(i)))
THMiter_via_intseg_split_pluck
Splitting the range of iteration.
f:(AAA), u:A.
is_ident(Afu)

is_assoc_sep(Af)

(a,c,b:e:({a..b}A).
(ac
(
(c<b
(
((Iter(f;ui:{a..b}. e(i))
(=
(f((Iter(f;ui:{a..c}. e(i)),f(e(c),Iter(f;ui:{c+1..b}. e(i))))
THMsum_via_intseg_split_pluck
Splitting the range of iteration.
a,c,b:e:({a..b}).
ac

c<b  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))+e(c)+( i:{c+1..b}. e(i))
THMmul_via_intseg_split_pluck
Splitting the range of iteration.
a,c,b:e:({a..b}).
ac

c<b  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))e(c)( i:{c+1..b}. e(i))
THMcomponents_divide_iter_mul
a,b:e:({a..b}), i:{a..b}. e(i) | ( i:{a..b}. e(i))
THMsum_via_intseg_split_mid
Splitting the range of iteration.
a,c,b:e:({a..b}).
ac  cb  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))+( i:{c..b}. e(i))
THMmul_via_intseg_split_mid
Splitting the range of iteration.
a,c,b:e:({a..b}).
ac  cb  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))( i:{c..b}. e(i))
THMsum_exponent
i:x,y:ixiy = i(x+y)
THMmul_via_intseg_split_last
a,b:e:({a..b}).
a<b  ( i:{a..b}. e(i)) = ( i:{a..b-1}. e(i))e(b-1)
THMmul_via_intseg_factors
a,b:f,g:({a..b}).
( i:{a..b}. f(i))( i:{a..b}. g(i)) = ( i:{a..b}. f(i)g(i))
THMexp_reduce1
Corollary to mul via intseg factors
a,b,c:. (ab)c = acbc
THMsum_via_intseg_split_last
a,b:e:({a..b}).
a<b  ( i:{a..b}. e(i)) = ( i:{a..b-1}. e(i))+e(b-1)
THMand_via_all_intseg_notnull
a,b:P:({a..b}Prop).
a<b  (c:b = c+1  ((i:{a..b}. P(i))  (i:{a..c}. P(i)) & P(c)))
THMand_via_all_intseg_split_last
a,b:P:({a..b}Prop).
a<b  ((i:{a..b}. P(i))  (i:{a..(b-1)}. P(i)) & P(b-1))
THMall_intseg_vs_iter_and
Universal quantification over a finite range is iterated conjunction.
a,b:P:({a..b}Prop). (i:{a..b}. P(i))  (And i:{a..b}. P(i))
THMor_via_exist_intseg_notnull
a,b:P:({a..b}Prop).
a<b  (c:b = c+1  ((i:{a..b}. P(i))  (i:{a..c}. P(i))  P(c)))
THMor_via_exist_intseg_split_last
a,b:P:({a..b}Prop).
a<b  ((i:{a..b}. P(i))  (i:{a..(b-1)}. P(i))  P(b-1))
THMexist_intseg_null
a,b:P:({a..b}Prop). ba  (i:{a..b}. P(i))
THMexist_intseg_vs_iter_or
Existential quantification over a finite range is iterated disjunction.
a,b:P:({a..b}Prop). (i:{a..b}. P(i))  (Or i:{a..b}. P(i))
THMiter_nat_prod_one_iff_factors_one
An iterated product is one iff each value is one.
e:({a..b}). ( i:{a..b}. e(i)) = 1  (i:{a..b}. e(i) = 1)
THMiter_prod_zero_iff_factor_zero
( i:{a..b}. e(i)) = 0  (i:{a..b}. e(i) = 0)
THMzero_ann_iter_via_intseg
(i:{a..b}. e(i) = 0)  ( i:{a..b}. e(i)) = 0
deffactorial_tail_via_iter
k!m ==  i:{k-m..k}. i+1
THMfactorial_tail_split_mid
n,m,k:nk-m  mk  k!(n+m) = (k-m)!nk!m
THMfactorial_tail_via_iter_null
m,k:m = 0    k!m = 1
THMfactorial_tail_via_iter_zero
m,k:k<m  k!m = 0
THMfactorial_tail_via_iter_step
m,k:. 1  m  k  (k',m':k' = k-1  m' = m-1  k!m = kk'!m'  )
THMfactorial_tail_via_iter_step_rw
m,k:. 1  m  k  k!m = k(k-1)!(m-1)
deffactorial_via_iter
k! == k!k
THMfactorial_ratio
m,k:mk  k! = (k-m)!k!m
THMfactorial_ratio2
Definition of a commonly used ratio of factorials.
m,k:mk  k!m = ((k!)  ((k-m)!))
THMmul_via_intseg_null
a,b:e:({a..b}). ba  ( i:{a..b}. e(i)) = 1
THMsum_via_intseg_null
a,b:e:({a..b}). ba  ( i:{a..b}. e(i)) = 0
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html