NatOrder.cv_2: def of bend-kit-collections@0.1.4.1 Import: import bend-kit-collections@0.1.4.1/nat_order.bend as NatOrder Lines 183-184 of bend-kit-collections@0.1.4.1/nat_order.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&start_line=183&end_line=184 import Base def cv_2(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {b == F(L{0n, 0n, 1n, 0n, 0n}, VS{a, b, c, d}) : Nat}: az2(b) Uses (5): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=F https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=Lin https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=Vs https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=az2