Thm* a,b: , e:({a..b }  ). b a  ( i:{a..b }. e(i)) = 0 | [sum_via_intseg_null] |
Thm* a,b: , e:({a..b }  ). b a  ( 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). b a  ( 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: , 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* a,c,b: , e:({a..b }  ).
Thm* a c
Thm* 
Thm* c b  ( 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* a c
Thm* 
Thm* c b  ( 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* a c
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* a c
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:(A A A), 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* (a c
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:(A A A), 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 d i  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:(A A A), 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* (a c
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)),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:(A A A), 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:(A A A), 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:(A A A), 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* a,b: , e:({a..b }  ). ( i:{a..b }. e(i) = 1)  ( i:{a..b }. e(i)) = 1 | [mul_via_intseg_one] |
Thm* f:(A A A), 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:(A A A), 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:(A A A), 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:(A A A), 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:(A A A), u:A, a,b: , e:({a..b } A).
Thm* b a  (Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) i:{a..a }. e(i)) | [iter_via_intseg_nullnorm] |
Thm* f:(A A A), u:A, a,b: , e:({a..b } A).
Thm* b a  (Iter(f;u) i:{a..b }. e(i)) = u | [iter_via_intseg_null] |
Thm* f:(A A A), 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...}. ( c:{a..b }. P(a,c))  P(a,b))  ( b:{a...}. P(a,b)) | [int_seg_upper_ind] |