def h.route_t

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

import Base

1933def h.route_t(
1934  +a: Bool, +c: Bool, +p: Nat, +xt: Word(p), +yt: Word(p), +mt: Word(p),
1935  +em: {h.isz(p, mt) == True{} : Bool},
1936  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},
1937  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}
1938) -> {Cmp.is_eq(Word.cmp.fin(Bool.and(a, True{}), Bool.and(c, True{}),
1939       Word.cmp(p, Word.and(p, xt, mt), Word.and(p, yt, mt)))) == True{} : Bool}:
1940  %Equal.sym(Bool, a, True{}, h.hd_true(a, p, xt, mt, em, ex))
1941    : {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}
1942  %Equal.sym(Bool, c, True{}, h.hd_true(c, p, yt, mt, em, ey))
1943    : {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}
1944  %Equal.sym(Cmp, Word.cmp(p, Word.and(p, xt, mt), Word.and(p, yt, mt)), EQ{}, h.zc2(p, xt, yt, mt, em))
1945    : {Cmp.is_eq(Word.cmp.fin(True{}, True{}, _)) == True{} : Bool}
1946  {==}