def h.route_w

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

import Base

1948def h.route_w(
1949  +n: Nat, x: Word(n), y: Word(n), m: Word(n),
1950  em: {h.at1(n, m) == True{} : Bool},
1951  ex: {Cmp.is_eq(Word.cmp(n, Word.and(n, x, m), Word.zero(n))) == False{} : Bool},
1952  ey: {Cmp.is_eq(Word.cmp(n, Word.and(n, y, m), Word.zero(n))) == False{} : Bool}
1953) -> {Cmp.is_eq(Word.cmp(n, Word.and(n, x, m), Word.and(n, y, m))) == True{} : Bool}:
1954  match n:
1955    case 0n:
1956      {==}
1957    case 1n+p:
1958      match x y m:
1959        case WCon{+a, +xt} WCon{+c, +yt} WCon{True{}, +mt}:
1960          h.route_t(a, c, p, xt, yt, mt, em, ex, ey)
1961        case WCon{+a, +xt} WCon{+c, +yt} WCon{False{}, +mt}:
1962          h.lift(a, c, Word.cmp(p, Word.and(p, xt, mt), Word.and(p, yt, mt)),
1963            h.route_w(p, xt, yt, mt, em,
1964              h.low(a, Word.cmp(p, Word.and(p, xt, mt), Word.zero(p)), ex),
1965              h.low(c, Word.cmp(p, Word.and(p, yt, mt), Word.zero(p)), ey)))