def h.hd_true

bend-kit-collections@0.1.4.1 · PROOF.bend:1877

import Base

1877# A head bit under a set mask bit, with the rest masked to zero, is set when the word is not zero.
1878def h.hd_true(
1879  a: Bool, +p: Nat, +xt: Word(p), +mt: Word(p), +em: {h.isz(p, mt) == True{} : Bool},
1880  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}
1881) -> {a == True{} : Bool}:
1882  match a:
1883    case True{}:
1884      {==}
1885    case False{}:
1886      Equal.sym(Bool, True{}, False{},
1887        rw(Cmp, t => {Cmp.is_eq(Word.cmp.fin(False{}, False{}, t)) == False{} : Bool},
1888          EQ{}, Word.cmp(p, Word.and(p, xt, mt), Word.zero(p)),
1889          Equal.sym(Cmp, Word.cmp(p, Word.and(p, xt, mt), Word.zero(p)), EQ{}, h.zc(p, xt, mt, em)), ex))