def top_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/gf.bend:164

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend as P

164def top_zero(+n: Nat) -> {P.top(n, Word.zero(n)) == False{} : Bool}:
165  match n:
166    case 0n:
167      {==}
168    case 1n:
169      {==}
170    case 2n+p:
171      top_zero(1n+p)