Thm* a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ). b a ![](FONT/eq.png) ( i:{a..b }. e(i)) = 0 | [sum_via_intseg_null] |
Thm* a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ). b a ![](FONT/eq.png) ( i:{a..b }. e(i)) = 1 | [mul_via_intseg_null] |
Thm* m,k: . m k ![](FONT/eq.png) k!m = ((k!) ((k-m)!)) | [factorial_ratio2] |
Thm* m,k: . m k ![](FONT/eq.png) k! = (k-m)! k!m | [factorial_ratio] |
Thm* m,k: . 1 m k ![](FONT/eq.png) k!m = k (k-1)!(m-1) ![](FONT/nat.png) | [factorial_tail_via_iter_step_rw] |
Thm* m,k: . 1 m k ![](FONT/eq.png) ( k',m': . k' = k-1 ![](FONT/eq.png) m' = m-1 ![](FONT/eq.png) k!m = k k'!m' ) | [factorial_tail_via_iter_step] |
Thm* m,k: . k<m ![](FONT/eq.png) k!m = 0 ![](FONT/nat.png) | [factorial_tail_via_iter_zero] |
Thm* m,k: . m = 0 ![](FONT/eq.png) k!m = 1 ![](FONT/nat.png) | [factorial_tail_via_iter_null] |
Thm* n,m,k: . n k-m ![](FONT/eq.png) m k ![](FONT/eq.png) k!(n+m) = (k-m)!n k!m | [factorial_tail_split_mid] |
Thm* ( i:{a..b }. e(i) = 0) ![](FONT/eq.png) ( i:{a..b }. e(i)) = 0 | [zero_ann_iter_via_intseg] |
Thm* a,b: , P:({a..b }![](FONT/dash.png) Prop). b a ![](FONT/eq.png) ( i:{a..b }. P(i)) | [exist_intseg_null] |
Thm* a,b: , P:({a..b }![](FONT/dash.png) Prop).
Thm* a<b ![](FONT/eq.png) (( i:{a..b }. P(i)) ![](FONT/if_big.png) ( i:{a..(b-1) }. P(i)) P(b-1)) | [or_via_exist_intseg_split_last] |
Thm* a,b: , P:({a..b }![](FONT/dash.png) Prop).
Thm* a<b
Thm* ![](FONT/eq.png)
Thm* ( c: . b = c+1 ![](FONT/eq.png) (( i:{a..b }. P(i)) ![](FONT/if_big.png) ( i:{a..c }. P(i)) P(c))) | [or_via_exist_intseg_notnull] |
Thm* a,b: , P:({a..b }![](FONT/dash.png) Prop).
Thm* a<b ![](FONT/eq.png) (( i:{a..b }. P(i)) ![](FONT/if_big.png) ( i:{a..(b-1) }. P(i)) & P(b-1)) | [and_via_all_intseg_split_last] |
Thm* a,b: , P:({a..b }![](FONT/dash.png) Prop).
Thm* a<b
Thm* ![](FONT/eq.png)
Thm* ( c: . b = c+1 ![](FONT/eq.png) (( i:{a..b }. P(i)) ![](FONT/if_big.png) ( i:{a..c }. P(i)) & P(c))) | [and_via_all_intseg_notnull] |
Thm* a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* a<b ![](FONT/eq.png) ( i:{a..b }. e(i)) = ( i:{a..b-1 }. e(i))+e(b-1) | [sum_via_intseg_split_last] |
Thm* a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* a<b ![](FONT/eq.png) ( 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 }![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* a c
Thm* ![](FONT/eq.png)
Thm* c b ![](FONT/eq.png) ( 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 }![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* a c
Thm* ![](FONT/eq.png)
Thm* c b ![](FONT/eq.png) ( i:{a..b }. e(i)) = ( i:{a..c }. e(i))+( i:{c..b }. e(i)) | [sum_via_intseg_split_mid] |
Thm* a,c,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* a c
Thm* ![](FONT/eq.png)
Thm* c<b
Thm* ![](FONT/eq.png)
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 }![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* a c
Thm* ![](FONT/eq.png)
Thm* c<b
Thm* ![](FONT/eq.png)
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![](FONT/dash.png) A![](FONT/dash.png) A), u:A.
Thm* is_ident(A; f; u)
Thm* ![](FONT/eq.png)
Thm* is_assoc_sep(A; f)
Thm* ![](FONT/eq.png)
Thm* ( a,c,b: , e:({a..b }![](FONT/dash.png) A).
Thm* (a c
Thm* (![](FONT/eq.png)
Thm* (c<b
Thm* (![](FONT/eq.png)
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![](FONT/dash.png) A![](FONT/dash.png) A), u:A.
Thm* is_ident(A; f; u)
Thm* ![](FONT/eq.png)
Thm* is_assoc_sep(A; f)
Thm* ![](FONT/eq.png)
Thm* ( a,b: , c:{a...b}, d:{c..b }, e:({a..b }![](FONT/dash.png) A).
Thm* (( i:{a..b }. i<c d i ![](FONT/eq.png) e(i) = u)
Thm* (![](FONT/eq.png)
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![](FONT/dash.png) A![](FONT/dash.png) A), u:A.
Thm* is_ident(A; f; u)
Thm* ![](FONT/eq.png)
Thm* is_assoc_sep(A; f)
Thm* ![](FONT/eq.png)
Thm* ( a,c,b: , e:({a..b }![](FONT/dash.png) A).
Thm* (a c
Thm* (![](FONT/eq.png)
Thm* (c b
Thm* (![](FONT/eq.png)
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* f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A.
Thm* is_commutative_sep(A; f)
Thm* ![](FONT/eq.png)
Thm* is_ident(A; f; u)
Thm* ![](FONT/eq.png)
Thm* is_assoc_sep(A; f)
Thm* ![](FONT/eq.png)
Thm* ( a,b: , e,g:({a..b }![](FONT/dash.png) 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![](FONT/dash.png) A![](FONT/dash.png) A), u:A, a,b,c,d: .
Thm* b-a = d-c
Thm* ![](FONT/eq.png)
Thm* ( e:({a..b }![](FONT/dash.png) A), g:({c..d }![](FONT/dash.png) A).
Thm* (( i:{a..b }, j:{c..d }. j-i = c-a ![](FONT/eq.png) e(i) = g(j) A)
Thm* (![](FONT/eq.png)
Thm* ((Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) j:{c..d }. g(j))) | [iter_via_intseg_shift] |
Thm* a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ). ( i:{a..b }. e(i) = 1) ![](FONT/eq.png) ( i:{a..b }. e(i)) = 1 | [mul_via_intseg_one] |
Thm* f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A.
Thm* is_ident(A; f; u)
Thm* ![](FONT/eq.png)
Thm* ( a,b: , e:({a..b }![](FONT/dash.png) A).
Thm* (( i:{a..b }. e(i) = u) ![](FONT/eq.png) (Iter(f;u) i:{a..b }. e(i)) = u) | [iter_via_intseg_all_units] |
Thm* f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A, a,b: , e:({a..b }![](FONT/dash.png) A).
Thm* a<b
Thm* ![](FONT/eq.png)
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 }![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* a<b ![](FONT/eq.png) ( c: . b = c+1 ![](FONT/eq.png) ( i:{a..b }. e(i)) = ( i:{a..c }. e(i))+e(c)) | [sum_via_intseg_notnull] |
Thm* a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* a<b ![](FONT/eq.png) ( c: . b = c+1 ![](FONT/eq.png) ( i:{a..b }. e(i)) = ( i:{a..c }. e(i)) e(c)) | [mul_via_intseg_notnull] |
Thm* f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A, a,b: , e:({a..b }![](FONT/dash.png) A).
Thm* a<b
Thm* ![](FONT/eq.png)
Thm* ( c: .
Thm* (b = c+1
Thm* (![](FONT/eq.png)
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 }![](FONT/dash.png) ![](FONT/then_med.png) ). a+1 = b ![](FONT/eq.png) ( i:{a..b }. e(i)) = e(a) | [mul_via_intseg_singleton] |
Thm* a,b: , e:({a..b }![](FONT/dash.png) ![](FONT/then_med.png) ). a+1 = b ![](FONT/eq.png) ( i:{a..b }. e(i)) = e(a) | [sum_via_intseg_singleton] |
Thm* f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A.
Thm* is_ident(A; f; u)
Thm* ![](FONT/eq.png)
Thm* ( a,b: , e:({a..b }![](FONT/dash.png) A). a+1 = b ![](FONT/eq.png) (Iter(f;u) i:{a..b }. e(i)) = e(a)) | [iter_via_intseg_singleton] |
Thm* f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A, a,b: , e:({a..b }![](FONT/dash.png) A).
Thm* b a ![](FONT/eq.png) (Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) i:{a..a }. e(i)) | [iter_via_intseg_nullnorm] |
Thm* f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u:A, a,b: , e:({a..b }![](FONT/dash.png) A).
Thm* b a ![](FONT/eq.png) (Iter(f;u) i:{a..b }. e(i)) = u | [iter_via_intseg_null] |
Thm* P:(![](FONT/int.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/int.png) ![](FONT/dash.png) Prop).
Thm* ( a: , b:{...a}. P(a,b))
Thm* ![](FONT/eq.png)
Thm* ( a: , b:{a+1...}. ( c:{a..b }. P(a,c)) ![](FONT/eq.png) P(a,b)) ![](FONT/eq.png) ( a,b: . P(a,b)) | [all_int_segs_by_upper_ind] |
Thm* P:(![](FONT/int.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/int.png) ![](FONT/dash.png) Prop), a: .
Thm* ( b:{...a}. P(a,b))
Thm* ![](FONT/eq.png)
Thm* ( b:{a+1...}. ( c:{a..b }. P(a,c)) ![](FONT/eq.png) P(a,b)) ![](FONT/eq.png) ( b: . P(a,b)) | [int_segs_from_base_by_upper_ind] |
Thm* P:(![](FONT/int.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/int.png) ![](FONT/dash.png) Prop), a: .
Thm* ( b:{...a}. P(a,a) ![](FONT/eq.png) P(a,b)) ![](FONT/eq.png) ( b:{a...}. P(a,b)) ![](FONT/eq.png) ( b: . P(a,b)) | [split_int_domain_by_norm_lower] |
Thm* P:(![](FONT/int.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/int.png) ![](FONT/dash.png) Prop), a: .
Thm* ( b:{a...}. ( c:{a..b }. P(a,c)) ![](FONT/eq.png) P(a,b)) ![](FONT/eq.png) ( b:{a...}. P(a,b)) | [int_seg_upper_ind] |
Thm* P:(![](FONT/int.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/int.png) ![](FONT/dash.png) Prop).
Thm* ( a: , b:{...a}. P(a,b))
Thm* ![](FONT/eq.png)
Thm* ( a: . ( b:{...a}. P(a,b)) ![](FONT/eq.png) ( b:{a...}. P(a,b))) ![](FONT/eq.png) ( a,b: . P(a,b)) | [all_int_pairs_via_all_splits] |
Thm* P:(![](FONT/int.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/int.png) ![](FONT/dash.png) Prop), a: .
Thm* ( b:{...a}. P(a,b))
Thm* ![](FONT/eq.png)
Thm* (( b:{...a}. P(a,b)) ![](FONT/eq.png) ( b:{a...}. P(a,b))) ![](FONT/eq.png) ( b: . P(a,b)) | [split_int_domain] |
Thm* f:(A![](FONT/dash.png) A![](FONT/dash.png) A), u,v:A. is_ident(A; f; u) ![](FONT/eq.png) is_ident(A; f; v) ![](FONT/eq.png) u = v | [binary_ident_unique] |