def zero_word

bend-collections-laws-math@1.0.0.0 · proofs/math/random/uint64n.bend:312

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as UA

312def zero_word(+n: WU.U64, +h: {X.is_zero(n) == True{} : Bool}) -> {n == Z() : WU.U64}:
313  match n:
314    case WU.U64{+l, +hh}:
315      +el = UA.eq_of(l, 0, L.and_left(U32.is_zero(l), U32.is_zero(hh), h))
316      +eh = UA.eq_of(hh, 0, L.and_right(U32.is_zero(l), U32.is_zero(hh), h))
317      %Equal.sym(U32, l, 0, el) : {WU.U64{_, hh} == Z() : WU.U64}
318      %Equal.sym(U32, hh, 0, eh) : {WU.U64{0, _} == Z() : WU.U64}
319      {==}