(* Sum1 and Sum use subtraction *)
-inline procedural "cic:/CoRN/algebra/CSums/Sumlist.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sumlist.con" as definition.
-inline procedural "cic:/CoRN/algebra/CSums/Sumx.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sumx.con" as definition.
(*#*
It is sometimes useful to view a function defined on $\{0,\ldots,i-1\}$
[Zero] when the input is greater than or equal to [i].
*)
-inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun.con".
+inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun.con" as definition.
-inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch1.con".
+inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch1.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch2.con".
+inline procedural "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch2.con" as lemma.
(*#* [Sum0] defines the sum for [i=0..(n-1)] *)
-inline procedural "cic:/CoRN/algebra/CSums/Sum0.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum0.con" as definition.
(*#* [Sum1] defines the sum for [i=m..(n-1)] *)
-inline procedural "cic:/CoRN/algebra/CSums/Sum1.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum1.con" as definition.
-inline procedural "cic:/CoRN/algebra/CSums/Sum.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum.con" as definition.
(* Sum i=m..n *)
(*#* [Sum2] is similar to [Sum1], but does not require the summand to be
defined outside where it is being added. *)
-inline procedural "cic:/CoRN/algebra/CSums/Sum2.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum2.con" as definition.
-inline procedural "cic:/CoRN/algebra/CSums/Sum_one.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_one.con" as lemma.
(* UNEXPORTED
Hint Resolve Sum_one: algebra.
*)
-inline procedural "cic:/CoRN/algebra/CSums/Sum_empty.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_empty.con" as lemma.
(* UNEXPORTED
Hint Resolve Sum_empty: algebra.
*)
-inline procedural "cic:/CoRN/algebra/CSums/Sum_Sum.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_Sum.con" as lemma.
(* UNEXPORTED
Hint Resolve Sum_Sum: algebra.
*)
-inline procedural "cic:/CoRN/algebra/CSums/Sum_first.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_first.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum_last.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_last.con" as lemma.
(* UNEXPORTED
Hint Resolve Sum_last: algebra.
*)
-inline procedural "cic:/CoRN/algebra/CSums/Sum_last'.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_last'.con" as lemma.
(*#*
We add some extensionality results which will be quite useful
when working with integration.
*)
-inline procedural "cic:/CoRN/algebra/CSums/Sum0_strext.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum0_strext.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum_strext.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_strext.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sumx_strext.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sumx_strext.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum0_strext'.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum0_strext'.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum_strext'.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_strext'.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum0_wd.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum0_wd.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum_wd.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_wd.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sumx_wd.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sumx_wd.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum_wd'.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_wd'.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum2_wd.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum2_wd.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum0_plus_Sum0.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum0_plus_Sum0.con" as lemma.
(* UNEXPORTED
Hint Resolve Sum0_plus_Sum0: algebra.
*)
-inline procedural "cic:/CoRN/algebra/CSums/Sum_plus_Sum.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_plus_Sum.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sumx_plus_Sumx.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sumx_plus_Sumx.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum2_plus_Sum2.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum2_plus_Sum2.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/inv_Sum0.con".
+inline procedural "cic:/CoRN/algebra/CSums/inv_Sum0.con" as lemma.
(* UNEXPORTED
Hint Resolve inv_Sum0: algebra.
*)
-inline procedural "cic:/CoRN/algebra/CSums/inv_Sum.con".
+inline procedural "cic:/CoRN/algebra/CSums/inv_Sum.con" as lemma.
(* UNEXPORTED
Hint Resolve inv_Sum: algebra.
*)
-inline procedural "cic:/CoRN/algebra/CSums/inv_Sumx.con".
+inline procedural "cic:/CoRN/algebra/CSums/inv_Sumx.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/inv_Sum2.con".
+inline procedural "cic:/CoRN/algebra/CSums/inv_Sum2.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum_minus_Sum.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_minus_Sum.con" as lemma.
(* UNEXPORTED
Hint Resolve Sum_minus_Sum: algebra.
*)
-inline procedural "cic:/CoRN/algebra/CSums/Sumx_minus_Sumx.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sumx_minus_Sumx.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum2_minus_Sum2.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum2_minus_Sum2.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum_apzero.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_apzero.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum_zero.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_zero.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum_term.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_term.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum0_shift.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum0_shift.con" as lemma.
(* UNEXPORTED
Hint Resolve Sum0_shift: algebra.
*)
-inline procedural "cic:/CoRN/algebra/CSums/Sum_shift.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_shift.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sum_big_shift.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sum_big_shift.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sumx_Sum0.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sumx_Sum0.con" as lemma.
(* UNEXPORTED
End Sums
alias id "G" = "cic:/CoRN/algebra/CSums/More_Sums/G.var".
-inline procedural "cic:/CoRN/algebra/CSums/Mengolli_Sum.con".
+inline procedural "cic:/CoRN/algebra/CSums/Mengolli_Sum.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Mengolli_Sum_gen.con".
+inline procedural "cic:/CoRN/algebra/CSums/Mengolli_Sum_gen.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/str_Mengolli_Sum_gen.con".
+inline procedural "cic:/CoRN/algebra/CSums/str_Mengolli_Sum_gen.con" as lemma.
-inline procedural "cic:/CoRN/algebra/CSums/Sumx_to_Sum.con".
+inline procedural "cic:/CoRN/algebra/CSums/Sumx_to_Sum.con" as lemma.
(* UNEXPORTED
End More_Sums