law bt2_bidx

lawful-bytes@0.1.1.0 · proof_fast_w2.bend:905

import Base
import lawful-bytes@0.1.1.0/fast.bend as FA

905law bt2_bidx:
906  for +e0: Bool
907  for +e1: Bool
908  for +e2: Bool
909  for +e3: Bool
910  for +f0: Bool
911  for +f1: Bool
912  for +f2: Bool
913  for +f3: Bool
914  for +h: {Nat.is_lt(Nat.min(R4(e0, e1, e2, e3), R4(f0, f1, f2, f3)), 4n) == True{} : Bool}
915  {U32.to_nat(U32.add(U32.add(FA.b2u(Bool.and(Bool.and(Bool.not(e0), True{}), Bool.and(Bool.not(f0), True{}))), FA.b2u(Bool.and(Bool.and(Bool.not(e0), Bool.and(Bool.not(e1), True{})), Bool.and(Bool.not(f0), Bool.and(Bool.not(f1), True{}))))), FA.b2u(Bool.and(Bool.and(Bool.not(e0), Bool.and(Bool.not(e1), Bool.and(Bool.not(e2), True{}))), Bool.and(Bool.not(f0), Bool.and(Bool.not(f1), Bool.and(Bool.not(f2), True{}))))))) == Nat.min(R4(e0, e1, e2, e3), R4(f0, f1, f2, f3)) : Nat}