PROOF.bits.word_bytes: def of bend-osdev-mode-core@0.1.0.0
Import: import bend-osdev-mode-core@0.1.0.0/PROOF.bend as PROOF
Lines 28-31 of bend-osdev-mode-core@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&start_line=28&end_line=31

import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M

def bits.word_bytes(w: U32) -> {M.cm.word(M.cm.b0(w), M.cm.b1(w), M.cm.b2(w), M.cm.b3(w)) == w : U32}:
  match w:
    case U32{WCon{w0, WCon{w1, WCon{w2, WCon{w3, WCon{w4, WCon{w5, WCon{w6, WCon{w7, WCon{w8, WCon{w9, WCon{w10, WCon{w11, WCon{w12, WCon{w13, WCon{w14, WCon{w15, WCon{w16, WCon{w17, WCon{w18, WCon{w19, WCon{w20, WCon{w21, WCon{w22, WCon{w23, WCon{w24, WCon{w25, WCon{w26, WCon{w27, WCon{w28, WCon{w29, WCon{w30, WCon{w31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
      {==}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.b0
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.b1
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.b2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.b3
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.word