def wsh.f20
bend-osdev-word64@0.1.1.0 · PROOF_text.bend:538
import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
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/word64.bend as W
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO
538def wsh.f20(+a: W.W64) -> {W.W64.is_zero(wsh.it(20n, a)) == True{} : Bool}:
539 wsh.vz(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))))), wsh.lz(W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))))), 64n, W.W64.to_nat(a), Equal.trans(Bool, Nat.is_le(Nat.double(U.U32Nat.dbl(64n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))))))), W.W64.to_nat(a)), Nat.is_le(U.U32Nat.dbl(65n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))))))), W.W64.to_nat(a)), True{}, {==}, Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(65n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))))))), W.W64.to_nat(a)), Nat.is_le(U.U32Nat.dbl(52n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))))))), W.W64.to_nat(a)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_le(zz, W.W64.to_nat(a)), U.U32Nat.dbl(65n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))))))), U.U32Nat.dbl(52n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))))))), Equal.sym(Nat, U.U32Nat.dbl(52n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))))))), U.U32Nat.dbl(65n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))))))), Equal.trans(Nat, U.U32Nat.dbl(52n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))))))), U.U32Nat.dbl(Nat.add(52n, 13n), W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))))))), U.U32Nat.dbl(65n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))))))), UL.dbl_dbl(52n, 13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))))))), {==}))), UO.nat_le_trans(U.U32Nat.dbl(52n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))))))), U.U32Nat.dbl(52n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))), W.W64.to_nat(a), Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(52n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))))))), U.U32Nat.dbl(52n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))), Nat.is_le(U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))))))), W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))), True{}, UL.dbl_le(52n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))))))), W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))), wsh.b4(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))), Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(52n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))), W.W64.to_nat(a)), Nat.is_le(U.U32Nat.dbl(39n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))), W.W64.to_nat(a)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_le(zz, W.W64.to_nat(a)), U.U32Nat.dbl(52n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))), U.U32Nat.dbl(39n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))), Equal.sym(Nat, U.U32Nat.dbl(39n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))), U.U32Nat.dbl(52n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))), Equal.trans(Nat, U.U32Nat.dbl(39n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))), U.U32Nat.dbl(Nat.add(39n, 13n), W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))), U.U32Nat.dbl(52n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))), UL.dbl_dbl(39n, 13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))), {==}))), UO.nat_le_trans(U.U32Nat.dbl(39n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))), U.U32Nat.dbl(39n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))), W.W64.to_nat(a), Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(39n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))))))), U.U32Nat.dbl(39n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))), Nat.is_le(U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))), W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))), True{}, UL.dbl_le(39n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))))))), W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))), wsh.b4(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))), Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(39n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))), W.W64.to_nat(a)), Nat.is_le(U.U32Nat.dbl(26n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))), W.W64.to_nat(a)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_le(zz, W.W64.to_nat(a)), U.U32Nat.dbl(39n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))), U.U32Nat.dbl(26n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))), Equal.sym(Nat, U.U32Nat.dbl(26n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))), U.U32Nat.dbl(39n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))), Equal.trans(Nat, U.U32Nat.dbl(26n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))), U.U32Nat.dbl(Nat.add(26n, 13n), W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))), U.U32Nat.dbl(39n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))), UL.dbl_dbl(26n, 13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))), {==}))), UO.nat_le_trans(U.U32Nat.dbl(26n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))), U.U32Nat.dbl(26n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))), W.W64.to_nat(a), Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(26n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))))))), U.U32Nat.dbl(26n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))), Nat.is_le(U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))), W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))), True{}, UL.dbl_le(26n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))))))), W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))), wsh.b4(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))), Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(26n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))), W.W64.to_nat(a)), Nat.is_le(U.U32Nat.dbl(13n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))), W.W64.to_nat(a)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_le(zz, W.W64.to_nat(a)), U.U32Nat.dbl(26n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))), U.U32Nat.dbl(13n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))), Equal.sym(Nat, U.U32Nat.dbl(13n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))), U.U32Nat.dbl(26n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))), Equal.trans(Nat, U.U32Nat.dbl(13n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))), U.U32Nat.dbl(Nat.add(13n, 13n), W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))), U.U32Nat.dbl(26n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))), UL.dbl_dbl(13n, 13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))), {==}))), UO.nat_le_trans(U.U32Nat.dbl(13n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))), U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(a)))))), W.W64.to_nat(a), Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(13n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a))))))))))), U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(a))))))), Nat.is_le(U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))), W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(a)))))), True{}, UL.dbl_le(13n, U.U32Nat.dbl(13n, W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(wsh.q(a)))))))))), W.W64.to_nat(wsh.q(wsh.q(wsh.q(wsh.q(a)))))), wsh.b4(wsh.q(wsh.q(wsh.q(wsh.q(a)))))), wsh.b4(a)))))))))), wv.lt64(a)))