law tkw3

lawful-bytes@0.1.1.0 · proof_fast_w1.bend:629

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

629# The flags of the low 3 byte(s), as words of four bytes.
630law tkw3:
631  for +X0: Word(8n)
632  for +X1: Word(8n)
633  for +X2: Word(8n)
634  for +X3: Word(8n)
635  {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(), Z.app8(8n, Z.h8(), Word.zero(8n)))))) == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), Bool.and(Bool.not(Z.allz(8n, X2)), True{}))) : Bool}