def wsh.b4

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:515

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

515def 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}:
516  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)))))))