LAWS.to_nat_parts: law of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/LAWS.bend as LAWS
Lines 70-75 of bend-osdev-word64@0.1.1.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&start_line=70&end_line=75

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-word64@0.1.1.0/word64.bend as W

# The value of a word (for every word): lo + hi * 2^32, the weight 2^32 being
# 32 doublings (U32Nat.dbl, from bend-osdev-u32).
law to_nat_parts:
  for +h: U32
  for +l: U32
  {W.W64.to_nat(W.W64.from_parts(h, l)) == Nat.add(U32.to_nat(l), U.U32Nat.dbl(32n, U32.to_nat(h))) : Nat}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.from_parts
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.to_nat