ProofFastW2.bt2_none: law of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_fast_w2.bend as ProofFastW2
Lines 379-388 of lawful-bytes@0.1.1.0/proof_fast_w2.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_w2.bend&start_line=379&end_line=388

import Base

law bt2_none:
  for +e0: Bool
  for +e1: Bool
  for +e2: Bool
  for +e3: Bool
  for +f0: Bool
  for +f1: Bool
  for +f2: Bool
  for +f3: Bool
  {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}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.min
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_w2.bend&name=R4