law mrg

lawful-bytes@0.1.1.0 · proof_fast_append.bend:459

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

459law mrg:
460  for +lo: U32
461  for +hi: U32
462  for +sh: Nat
463  for +r: Nat
464  for +hsh: {sh == Nat.mul(8n, r) : Nat}
465  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
466  {U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh))) == W.merge(lo, hi, r) : U32}