law band_perm

lawful-words@0.1.0.0 · proof_bytes.bend:29

import Base

29# and(a, and(b, and(c, d))) = and(b, and(a, d)) when a implies c.
30law band_perm:
31  for +a: Bool
32  for +b: Bool
33  for +c: Bool
34  for +d: Bool
35  for imp: {a == True{} : Bool} -> {c == True{} : Bool}
36  {Bool.and(a, Bool.and(b, Bool.and(c, d))) == Bool.and(b, Bool.and(a, d)) : Bool}