def top_ok

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixgen.bend:43

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

43# the largest w-bit value: it fits, its successor does not
44def top_ok(+w: Nat, +t: Nat, +h1: {C.fits(w, t) == True{} : Bool}, +h2: {C.fits(w, 1n+t) == False{} : Bool}) -> {Bool.and(C.fits(w, t), Bool.not(C.fits(w, 1n+t))) == True{} : Bool}:
45  %Equal.sym(Bool, C.fits(w, t), True{}, h1) : {Bool.and(_, Bool.not(C.fits(w, 1n+t))) == True{} : Bool}
46  %Equal.sym(Bool, C.fits(w, 1n+t), False{}, h2) : {Bool.and(True{}, Bool.not(_)) == True{} : Bool}
47  {==}