law op_four

bend-mathlib@0.8.1.0 · algebra.bend:55

import Base

55# Middle-four interchange from associativity and commutativity.
56law op_four:
57  for ~A: Data
58  for ~op: A -> A -> A
59  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
60  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
61  for +a: A
62  for +b: A
63  for +c: A
64  for +d: A
65  {op(op(a, b), op(c, d)) == op(op(a, c), op(b, d)) : A}