PROOFText.wsh.lz: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
Lines 531-536 of bend-osdev-word64@0.1.1.0/PROOF_text.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&start_line=531&end_line=536

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
import bend-osdev-word64@0.1.1.0/proof_value.bend as P
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

def wsh.lz(y: Nat, +N: Nat, +A: Nat, +h1: {Nat.is_le(Nat.double(U.U32Nat.dbl(N, y)), A) == True{} : Bool}, +h2: {Nat.is_lt(A, U.U32Nat.dbl(N, 1n)) == True{} : Bool}) -> {y == 0n : Nat}:
  match y:
    case 0n:
      {==}
    case 1n+ +p:
      Empty.absurd({1n+p == 0n : Nat}, P.wn.lt_irrefl(A, UO.nat_lt_le_trans(A, U.U32Nat.dbl(N, 1n), A, h2, UO.nat_le_trans(U.U32Nat.dbl(N, 1n), Nat.double(U.U32Nat.dbl(N, 1n+p)), A, Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(N, 1n), Nat.double(U.U32Nat.dbl(N, 1n+p))), Nat.is_le(U.U32Nat.dbl(N, 1n), Nat.add(Nat.add(U.U32Nat.dbl(N, 1n), Nat.double(U.U32Nat.dbl(N, p))), U.U32Nat.dbl(N, 1n))), True{}, Equal.sym(Bool, Nat.is_le(U.U32Nat.dbl(N, 1n), Nat.add(Nat.add(U.U32Nat.dbl(N, 1n), Nat.double(U.U32Nat.dbl(N, p))), U.U32Nat.dbl(N, 1n))), Nat.is_le(U.U32Nat.dbl(N, 1n), Nat.double(U.U32Nat.dbl(N, 1n+p))), Equal.cong(Nat, Bool, zz => Nat.is_le(U.U32Nat.dbl(N, 1n), zz), Nat.add(Nat.add(U.U32Nat.dbl(N, 1n), Nat.double(U.U32Nat.dbl(N, p))), U.U32Nat.dbl(N, 1n)), Nat.double(U.U32Nat.dbl(N, 1n+p)), wr.t16(N, p))), UL.nat_le_add(U.U32Nat.dbl(N, 1n), Nat.add(U.U32Nat.dbl(N, 1n), Nat.double(U.U32Nat.dbl(N, p))))), h1))))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  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=nat_le_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS_order.bend&name=nat_le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS_order.bend&name=nat_lt_le_trans
  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_text.bend&name=wr.t16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.lt_irrefl