PROOF.word.cmp_nat.h: def of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF
Lines 906-908 of bend-osdev-algo@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&start_line=906&end_line=908

import Base

def word.cmp_nat.h(+p: Nat, +x: Bool, +y: Bool, +at: Word(p), +bt: Word(p), ih: {Word.cmp(p, at, bt) == Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt)) : Cmp}) -> {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) == Nat.cmp(nat.dbit(x, Word.to_nat(p, at)), nat.dbit(y, Word.to_nat(p, bt))) : Cmp}:
  %Equal.sym(Cmp, Word.cmp(p, at, bt), Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt)), ih) : {Word.cmp.fin(x, y, _) == Nat.cmp(nat.dbit(x, Word.to_nat(p, at)), nat.dbit(y, Word.to_nat(p, bt))) : Cmp}
  word.cmp_nat.d(Word.to_nat(p, at), Word.to_nat(p, bt), x, y)

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.dbit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=word.cmp_nat.d