def Q5

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

import Base

162def Q5(+x: U32) -> INV(1n, v(x), S5(x)):
163  bstep2(1n, {==}, v(x), P1(S4(x)), P2(S4(x)), Q4(x))

Uses (9)