law tkw2

lawful-bytes@0.1.1.0 · proof_fast_w1.bend:607

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

607# The flags of the low 2 byte(s), as words of four bytes.
608law tkw2:
609  for +X0: Word(8n)
610  for +X1: Word(8n)
611  for +X2: Word(8n)
612  for +X3: Word(8n)
613  {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}