ProofFastW1.tkw2: law of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_fast_w1.bend as ProofFastW1
Lines 607-613 of lawful-bytes@0.1.1.0/proof_fast_w1.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_w1.bend&start_line=607&end_line=613

import Base
import lawful-words@0.1.0.0/proof_zb.bend as Z

# The flags of the low 2 byte(s), as words of four bytes.
law tkw2:
  for +X0: Word(8n)
  for +X1: Word(8n)
  for +X2: Word(8n)
  for +X3: Word(8n)
  {Z.allz(32n, Word.and(32n, Z.zf(32n, Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Word.zero(16n))))) == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), True{})) : Bool}

Uses (16):
  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=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_w1.bend&name=zbk_byte
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=allz
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=allz_andz
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=app8
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=h8
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=one8
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_zb.bend&name=zf