law op_assoc4

bend-mathlib@0.8.1.0 · algebra.bend:7

import Base

7# Four-way reassociation from associativity alone.
8law op_assoc4:
9  for ~A: Data
10  for ~op: A -> A -> A
11  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
12  for +a: A
13  for +b: A
14  for +c: A
15  for +d: A
16  {op(op(op(a, b), c), d) == op(a, op(b, op(c, d))) : A}