fact: Fixpoint clean_sum a x := match x with | zero => a | one => cplus a one | var i => cplus a (var i) | dot x1 x2 => cplus a (clean_prod (clean_prod one x1) x2) | plus x1 x2 => clean_sum (clean_sum a x1) x2 end with clean_prod a x := match x with | zero => zero | one => a | var i => cdot a (var i) | dot x1 x2 => clean_prod (clean_prod a x1) x2 | plus x1 x2 => cdot a (clean_sum (clean_sum zero x1) x2) end.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)