PROOF.h.isz: def of bend-kit-collections@0.1.4.1 Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF Lines 1820-1828 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=1820&end_line=1828 import Base # A mask with at most one set bit routes every hash to one of two sides. def h.isz(n: Nat, w: Word(n)) -> Bool: match n: case 0n: True{} case 1n+p: match w: case WCon{b, t}: Bool.not(b) && h.isz(p, t) Uses (6): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con