law finish_one

stelliferous@0.0.2.0 · proofs/word_encoding.bend:116

import Base

116law finish_one:
117  for +b: Bool
118  for +c: Cmp
119  for nonneg: {Cmp.is_lt(c) == False{} : Bool}
120  {Cmp.is_lt(Word.cmp.fin(b,True{},c)) == Cmp.is_eq(Word.cmp.fin(b,False{},c)) : Bool}