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

import Base

def h.route_t(
  +a: Bool, +c: Bool, +p: Nat, +xt: Word(p), +yt: 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},
  ey: {Cmp.is_eq(Word.cmp.fin(Bool.and(c, True{}), False{}, Word.cmp(p, Word.and(p, yt, mt), Word.zero(p)))) == False{} : Bool}
) -> {Cmp.is_eq(Word.cmp.fin(Bool.and(a, True{}), Bool.and(c, True{}),
       Word.cmp(p, Word.and(p, xt, mt), Word.and(p, yt, mt)))) == True{} : Bool}:
  %Equal.sym(Bool, a, True{}, h.hd_true(a, p, xt, mt, em, ex))
    : {Cmp.is_eq(Word.cmp.fin(Bool.and(_, True{}), Bool.and(c, True{}), Word.cmp(p, Word.and(p, xt, mt), Word.and(p, yt, mt)))) == True{} : Bool}
  %Equal.sym(Bool, c, True{}, h.hd_true(c, p, yt, mt, em, ey))
    : {Cmp.is_eq(Word.cmp.fin(True{}, Bool.and(_, True{}), Word.cmp(p, Word.and(p, xt, mt), Word.and(p, yt, mt)))) == True{} : Bool}
  %Equal.sym(Cmp, Word.cmp(p, Word.and(p, xt, mt), Word.and(p, yt, mt)), EQ{}, h.zc2(p, xt, yt, mt, em))
    : {Cmp.is_eq(Word.cmp.fin(True{}, True{}, _)) == True{} : Bool}
  {==}

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.hd_true
  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.zc2