#line 504 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
  Additive symmetric float-approximate group, symbol +.
  Note: associativity is not assumed.
  class FloatAddgrp[t] {
    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 +.
  class Addgrp[t] {
    inherit FloatAddgrp[t];
    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;
    }
  
  }