law op_assoc4_sym

bend-mathlib@0.8.1.0 · algebra.bend:294

import Base

294# Four-way reassociation from associativity alone, reversed to rewrite toward the simple side.
295law op_assoc4_sym:
296  for ~A: Data
297  for ~op: A -> A -> A
298  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
299  for +a: A
300  for +b: A
301  for +c: A
302  for +d: A
303  {op(a, op(b, op(c, d))) == op(op(op(a, b), c), d) : A}