law tkw1

lawful-bytes@0.1.1.0 · proof_fast_w1.bend:589

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

589# The flags of the low 1 byte(s), as words of four bytes.
590law tkw1:
591  for +X0: Word(8n)
592  for +X1: Word(8n)
593  for +X2: Word(8n)
594  for +X3: Word(8n)
595  {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(), Word.zero(24n)))) == Bool.and(Bool.not(Z.allz(8n, X0)), True{}) : Bool}