PROOFText.wsh.b4: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
Lines 515-516 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=515&end_line=516

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

def wsh.b4(+x: W.W64) -> {Nat.is_le(U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), W.W64.to_nat(x)) == True{} : Bool}:
  UO.nat_le_trans(U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), Nat.add(U.U32Nat.dbl(6n, Nat.add(U.U32Nat.dbl(6n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), U.U32Nat.dbl(5n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))))), U.U32Nat.dbl(5n, Nat.add(U.U32Nat.dbl(6n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), U.U32Nat.dbl(5n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x))))))))), W.W64.to_nat(x), wsh.gg(W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), UO.nat_le_trans(Nat.add(U.U32Nat.dbl(6n, Nat.add(U.U32Nat.dbl(6n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), U.U32Nat.dbl(5n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))))), U.U32Nat.dbl(5n, Nat.add(U.U32Nat.dbl(6n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), U.U32Nat.dbl(5n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x))))))))), Nat.add(U.U32Nat.dbl(6n, W.W64.to_nat(wsh.q(wsh.q(x)))), U.U32Nat.dbl(5n, W.W64.to_nat(wsh.q(wsh.q(x))))), W.W64.to_nat(x), wsh.gm(Nat.add(U.U32Nat.dbl(6n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), U.U32Nat.dbl(5n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x))))))), W.W64.to_nat(wsh.q(wsh.q(x))), UO.nat_le_trans(Nat.add(U.U32Nat.dbl(6n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), U.U32Nat.dbl(5n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x))))))), Nat.add(U.U32Nat.dbl(3n, Nat.add(U.U32Nat.dbl(3n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), U.U32Nat.dbl(1n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))))), U.U32Nat.dbl(1n, Nat.add(U.U32Nat.dbl(3n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), U.U32Nat.dbl(1n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x))))))))), W.W64.to_nat(wsh.q(wsh.q(x))), wsh.gf(W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), UO.nat_le_trans(Nat.add(U.U32Nat.dbl(3n, Nat.add(U.U32Nat.dbl(3n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), U.U32Nat.dbl(1n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))))), U.U32Nat.dbl(1n, Nat.add(U.U32Nat.dbl(3n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), U.U32Nat.dbl(1n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x))))))))), Nat.add(U.U32Nat.dbl(3n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(x))))), U.U32Nat.dbl(1n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(x)))))), W.W64.to_nat(wsh.q(wsh.q(x))), wsh.fm(Nat.add(U.U32Nat.dbl(3n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x)))))), U.U32Nat.dbl(1n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x))))))), W.W64.to_nat(wsh.q(wsh.q(wsh.q(x)))), wsh.f1(W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(x))))), U32.to_nat(wsh.r(wsh.q(wsh.q(wsh.q(x))))), W.W64.to_nat(wsh.q(wsh.q(wsh.q(x)))), wsd.e(wsh.q(wsh.q(wsh.q(x))), wsd.sd(wsh.q(wsh.q(wsh.q(x))))))), wsh.f1(W.W64.to_nat(wsh.q(wsh.q(wsh.q(x)))), U32.to_nat(wsh.r(wsh.q(wsh.q(x)))), W.W64.to_nat(wsh.q(wsh.q(x))), wsd.e(wsh.q(wsh.q(x)), wsd.sd(wsh.q(wsh.q(x)))))))), UO.nat_le_trans(Nat.add(U.U32Nat.dbl(6n, W.W64.to_nat(wsh.q(wsh.q(x)))), U.U32Nat.dbl(5n, W.W64.to_nat(wsh.q(wsh.q(x))))), Nat.add(U.U32Nat.dbl(3n, Nat.add(U.U32Nat.dbl(3n, W.W64.to_nat(wsh.q(wsh.q(x)))), U.U32Nat.dbl(1n, W.W64.to_nat(wsh.q(wsh.q(x)))))), U.U32Nat.dbl(1n, Nat.add(U.U32Nat.dbl(3n, W.W64.to_nat(wsh.q(wsh.q(x)))), U.U32Nat.dbl(1n, W.W64.to_nat(wsh.q(wsh.q(x))))))), W.W64.to_nat(x), wsh.gf(W.W64.to_nat(wsh.q(wsh.q(x)))), UO.nat_le_trans(Nat.add(U.U32Nat.dbl(3n, Nat.add(U.U32Nat.dbl(3n, W.W64.to_nat(wsh.q(wsh.q(x)))), U.U32Nat.dbl(1n, W.W64.to_nat(wsh.q(wsh.q(x)))))), U.U32Nat.dbl(1n, Nat.add(U.U32Nat.dbl(3n, W.W64.to_nat(wsh.q(wsh.q(x)))), U.U32Nat.dbl(1n, W.W64.to_nat(wsh.q(wsh.q(x))))))), Nat.add(U.U32Nat.dbl(3n, W.W64.to_nat(wsh.q(x))), U.U32Nat.dbl(1n, W.W64.to_nat(wsh.q(x)))), W.W64.to_nat(x), wsh.fm(Nat.add(U.U32Nat.dbl(3n, W.W64.to_nat(wsh.q(wsh.q(x)))), U.U32Nat.dbl(1n, W.W64.to_nat(wsh.q(wsh.q(x))))), W.W64.to_nat(wsh.q(x)), wsh.f1(W.W64.to_nat(wsh.q(wsh.q(x))), U32.to_nat(wsh.r(wsh.q(x))), W.W64.to_nat(wsh.q(x)), wsd.e(wsh.q(x), wsd.sd(wsh.q(x))))), wsh.f1(W.W64.to_nat(wsh.q(x)), U32.to_nat(wsh.r(x)), W.W64.to_nat(x), wsd.e(x, wsd.sd(x)))))))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.is_le
  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/LAWS_order.bend&name=nat_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=wsd.e
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsd.sd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.f1
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.fm
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.gf
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.gg
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.gm
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.q
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.r
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.to_nat