law bt_none

lawful-bytes@0.1.1.0 · proof_fast_w2.bend:294

import Base

294law bt_none:
295  for +e0: Bool
296  for +e1: Bool
297  for +e2: Bool
298  for +e3: Bool
299  {Bool.and(Bool.not(e0), Bool.and(Bool.not(e1), Bool.and(Bool.not(e2), Bool.not(e3)))) == Nat.is_eq(R4(e0, e1, e2, e3), 4n) : Bool}