law bt2_none

lawful-bytes@0.1.1.0 · proof_fast_w2.bend:379

import Base

379law bt2_none:
380  for +e0: Bool
381  for +e1: Bool
382  for +e2: Bool
383  for +e3: Bool
384  for +f0: Bool
385  for +f1: Bool
386  for +f2: Bool
387  for +f3: Bool
388  {Bool.and(Bool.and(Bool.not(e0), Bool.and(Bool.not(e1), Bool.and(Bool.not(e2), Bool.not(e3)))), Bool.and(Bool.not(f0), Bool.and(Bool.not(f1), Bool.and(Bool.not(f2), Bool.not(f3))))) == Nat.is_eq(Nat.min(R4(e0, e1, e2, e3), R4(f0, f1, f2, f3)), 4n) : Bool}