law op_comm3

bend-mathlib@0.8.1.0 · algebra.bend:73

import Base

73# Three-way commutation from commutativity alone.
74law op_comm3:
75  for ~A: Data
76  for ~op: A -> A -> A
77  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
78  for +a: A
79  for +b: A
80  for +c: A
81  {op(op(a, b), c) == op(c, op(b, a)) : A}