law mrg2

lawful-bytes@0.1.1.0 · proof_fast_append.bend:431

import Base
import lawful-words@0.1.0.0/defs.bend as W

431# The code's shifted pair is lawful-words' merge.
432law mrg2:
433  for +lo: U32
434  for +hi: U32
435  for +r: Nat
436  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
437  {U32.or(U32.shrn(lo, Nat.mul(8n, r)), U32.shln(hi, Nat.sub(32n, Nat.mul(8n, r)))) == W.merge(lo, hi, r) : U32}