def isfin_g

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bits.bend:264

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

264def isfin_g(+one: Nat, +h1: {one == 1n : Nat}, +l: U32, +h: U32, +c20: U32, +hc20: {c20 == U32{WD.pw(32n, 20n)} : U32}, +m11: U32, +hm11: {m11 == U32{WD.mask(32n, 11n)} : U32}) -> {Nat.is_lt(v(U32.and(U32.div(h, c20), m11)), 2047n) == Bool.not(Nat.is_eq(SF.efield(F.Bits{l, h}), 2047n)) : Bool}:
265  +ei = v(U32.and(U32.div(h, c20), m11))
266  +es = SF.efield(F.Bits{l, h})
267  Equal.trans(Bool, Nat.is_lt(ei, 2047n), Nat.is_lt(es, 2047n), Bool.not(Nat.is_eq(es, 2047n)), Equal.cong(Nat, Bool, z => Nat.is_lt(z, 2047n), ei, es, ef_g(one, h1, h, c20, hc20, m11, hm11)), lt_ne(es, 2047n, WW.low_lt(11n, C.high(20n, v(h)))))