ProofValue.wv.ncmp: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/proof_value.bend as ProofValue
Lines 324-338 of bend-osdev-word64@0.1.1.0/proof_value.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&start_line=324&end_line=338

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

def wv.ncmp(+n: Nat, ah: Nat, bh: Nat, +al: Nat, +bl: Nat, hal: {Nat.is_lt(al, U.U32Nat.dbl(n, 1n)) == True{} : Bool}, hbl: {Nat.is_lt(bl, U.U32Nat.dbl(n, 1n)) == True{} : Bool}) -> {wv.lex(Nat.cmp(ah, bh), Nat.cmp(al, bl)) == Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, ah)), Nat.add(bl, U.U32Nat.dbl(n, bh))) : Cmp}:
  match ah bh:
    case 0n 0n:
      Equal.sym(Cmp, Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 0n))), Nat.cmp(al, bl), wv.ncmp0(n, al, bl))
    case 0n 1n+ +q:
      Equal.sym(Cmp, Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 1n+q))), LT{}, wn.lt_of(Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 1n+q))), wv.nlt(n, al, bl, q, hal)))
    case 1n+ +p 0n:
      Equal.sym(Cmp, Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, 1n+p)), Nat.add(bl, U.U32Nat.dbl(n, 0n))), GT{}, wn.cmp_gt(Nat.add(al, U.U32Nat.dbl(n, 1n+p)), Nat.add(bl, U.U32Nat.dbl(n, 0n)), wv.nlt(n, bl, al, p, hbl)))
    case 1n+ +p 1n+ +q:
      +ea = Equal.trans(Nat, Nat.add(al, U.U32Nat.dbl(n, 1n+p)), Nat.add(al, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p))), Equal.cong(Nat, Nat, v => Nat.add(al, v), U.U32Nat.dbl(n, 1n+p), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p)), UL.dbl_add(n, 1n, p)), UL.nat_add_left_comm(al, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p)))
      +eb = Equal.trans(Nat, Nat.add(bl, U.U32Nat.dbl(n, 1n+q)), Nat.add(bl, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(bl, U.U32Nat.dbl(n, q))), Equal.cong(Nat, Nat, v => Nat.add(bl, v), U.U32Nat.dbl(n, 1n+q), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q)), UL.dbl_add(n, 1n, q)), UL.nat_add_left_comm(bl, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q)))
      %Equal.sym(Nat, Nat.add(al, U.U32Nat.dbl(n, 1n+p)), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p))), ea) : {wv.lex(Nat.cmp(p, q), Nat.cmp(al, bl)) == Nat.cmp(_, Nat.add(bl, U.U32Nat.dbl(n, 1n+q))) : Cmp}
      %Equal.sym(Nat, Nat.add(bl, U.U32Nat.dbl(n, 1n+q)), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(bl, U.U32Nat.dbl(n, q))), eb) : {wv.lex(Nat.cmp(p, q), Nat.cmp(al, bl)) == Nat.cmp(Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p))), _) : Cmp}
      %Equal.sym(Cmp, Nat.cmp(Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(bl, U.U32Nat.dbl(n, q)))), Nat.cmp(Nat.add(al, U.U32Nat.dbl(n, p)), Nat.add(bl, U.U32Nat.dbl(n, q))), wn.cmp_add_l(U.U32Nat.dbl(n, 1n), Nat.add(al, U.U32Nat.dbl(n, p)), Nat.add(bl, U.U32Nat.dbl(n, q)))) : {wv.lex(Nat.cmp(p, q), Nat.cmp(al, bl)) == _ : Cmp}
      wv.ncmp(n, p, q, al, bl, hal, hbl)

Uses (18):
  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.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=Nat.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_left_comm
  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/proof_value.bend&name=wn.cmp_add_l
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.cmp_gt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.lt_of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wv.lex
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wv.ncmp0
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wv.nlt