PROOF.h.hd_true: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 1877-1889 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=1877&end_line=1889

import Base

# A head bit under a set mask bit, with the rest masked to zero, is set when the word is not zero.
def h.hd_true(
  a: Bool, +p: Nat, +xt: Word(p), +mt: Word(p), +em: {h.isz(p, mt) == True{} : Bool},
  ex: {Cmp.is_eq(Word.cmp.fin(Bool.and(a, True{}), False{}, Word.cmp(p, Word.and(p, xt, mt), Word.zero(p)))) == False{} : Bool}
) -> {a == True{} : Bool}:
  match a:
    case True{}:
      {==}
    case False{}:
      Equal.sym(Bool, True{}, False{},
        rw(Cmp, t => {Cmp.is_eq(Word.cmp.fin(False{}, False{}, t)) == False{} : Bool},
          EQ{}, Word.cmp(p, Word.and(p, xt, mt), Word.zero(p)),
          Equal.sym(Cmp, Word.cmp(p, Word.and(p, xt, mt), Word.zero(p)), EQ{}, h.zc(p, xt, mt, em)), ex))

Uses (14):
  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=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.isz
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.zc
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=rw