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

import Base

def h.route_w(
  +n: Nat, x: Word(n), y: Word(n), m: Word(n),
  em: {h.at1(n, m) == True{} : Bool},
  ex: {Cmp.is_eq(Word.cmp(n, Word.and(n, x, m), Word.zero(n))) == False{} : Bool},
  ey: {Cmp.is_eq(Word.cmp(n, Word.and(n, y, m), Word.zero(n))) == False{} : Bool}
) -> {Cmp.is_eq(Word.cmp(n, Word.and(n, x, m), Word.and(n, y, m))) == True{} : Bool}:
  match n:
    case 0n:
      {==}
    case 1n+p:
      match x y m:
        case WCon{+a, +xt} WCon{+c, +yt} WCon{True{}, +mt}:
          h.route_t(a, c, p, xt, yt, mt, em, ex, ey)
        case WCon{+a, +xt} WCon{+c, +yt} WCon{False{}, +mt}:
          h.lift(a, c, Word.cmp(p, Word.and(p, xt, mt), Word.and(p, yt, mt)),
            h.route_w(p, xt, yt, mt, em,
              h.low(a, Word.cmp(p, Word.and(p, xt, mt), Word.zero(p)), ex),
              h.low(c, Word.cmp(p, Word.and(p, yt, mt), Word.zero(p)), ey)))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=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.Con
  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.zero
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.at1
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.lift
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.low
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.route_t