def Q4

import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64clz.bend as W64clz

import Base

159def Q4(+x: U32) -> INV(2n, v(x), S4(x)):
160  bstep2(2n, {==}, v(x), P1(S3(x)), P2(S3(x)), Q3(x))

Uses (9)