def Q2

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

import Base

153def Q2(+x: U32) -> INV(8n, v(x), S2(x)):
154  bstep2(8n, {==}, v(x), P1(S1(x)), P2(S1(x)), Q1(x))

Uses (9)