law zb_byte

lawful-words@0.1.0.0 · proof_zb.bend:84

import Base

84# One byte of the zero-byte test, with no borrow in.
85law zb_byte:
86  for +n: Nat
87  for +x: Word(8n)
88  for +r: Word(n)
89  for +kr: Word(n)
90  for +hr: Word(n)
91  {allz(Nat.add(8n, n), zf(Nat.add(8n, n), app8(n, x, r), app8(n, one8(), kr), app8(n, h8(), hr), True{}))
92    == Bool.and(Bool.not(allz(8n, x)), allz(n, zf(n, r, kr, hr, True{}))) : Bool}