#line 504 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
Additive symmetric float-approximate group, symbol +.
Note: associativity is not assumed.
inherit Eq[t];
virtual fun zero: unit -> t;
virtual fun + : t * t -> t;
virtual fun neg : t -> t;
virtual fun prefix_plus : t -> t = "\$1";
virtual fun - (x:t,y:t):t => x + -y;
virtual proc += (px:&t,y:t) { px <- *px + y; }
virtual proc -= (px:&t,y:t) { px <- *px - y; }

reduce id (x:t): x+zero() => x;
reduce id (x:t): zero()+x => x;
reduce inv(x:t): x - x => zero();
reduce inv(x:t): - (-x) => x;
axiom sym (x:t,y:t): x+y == y+x;

fun add(x:t,y:t)=> x + y;
fun plus(x:t)=> +x;
fun sub(x:t,y:t)=> x - y;
proc pluseq(px:&t, y:t) {  += (px,y); }
proc  minuseq(px:&t, y:t) { -= (px,y); }
}
#line 545 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
Additive symmetric group, symbol +.
axiom assoc (x:t,y:t,z:t): (x + y) + z == x + (y + z);
reduce inv(x:t,y:t): x + y - y => x;
}

#line 556 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
Multiplicative symmetric float-approximate semi group with unit symbol *.
Note: associativity is not assumed.
class FloatMultSemi1[t] {
inherit Eq[t];
proc muleq(px:&t, y:t) { *= (px,y); }
fun mul(x:t, y:t) => x * y;
fun sqr(x:t) => x * x;
fun cube(x:t) => x * x * x;
virtual fun one: unit -> t;
virtual fun * : t * t -> t;
virtual proc *= (px:&t, y:t) { px <- *px * y; }
reduce id (x:t): x*one() => x;
reduce id (x:t): one()*x => x;
}

#line 585 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
Multiplicative semi group with unit.
class MultSemi1[t] {
inherit FloatMultSemi1[t];
axiom assoc (x:t,y:t,z:t): (x * y) * z == x * (y * z);
reduce cancel (x:t,y:t,z:t): x * z ==  y * z => x == y;
}

#line 893 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
open class Quantifiers_add_mul {
fun $$\sum$$[T,C with FloatAddgrp[T], Streamable[C,T]] (a:C):T =
{
var init = #zero[T];
for x in a perform init = init + x;
return init;
}

fun $$\prod$$[T,C with FloatMultSemi1[T], Streamable[C,T]] (a:C):T =
{
var init = #one[T];
for x in a perform init = init * x;
return init;
}

fun $$\sum$$[T with FloatAddgrp[T]] (f:1->opt[T])  =
{
var init = #zero[T];
for x in f perform init = init + x;
return init;
}

fun $$\prod$$[T with FloatMultSemi1[T]] (f:1->opt[T])  =
{
var init = #one[T];
for x in f perform init = init * x;
return init;
}

}