def lt_gen

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64cmp.bend:304

import Base
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/math/typed/f64bits.bend as FB

304def lt_gen(+one: Nat, +h1: {one == 1n : Nat}, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +bad: Bool, +hbad: {Bool.or(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh})) == bad : Bool}, +z: Bool) -> {F.lt_z(F.Bits{xl, xh}, F.Bits{yl, yh}, bad, z) == Bool.and(Bool.not(bad), Cmp.is_lt(SF.pick(Cmp, z, EQ{}, SF.pick(Cmp, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), SF.pick(Cmp, SF.sign(F.Bits{xl, xh}), SF.flip(SF.mag_cmp(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.mag_cmp(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.pick(Cmp, SF.sign(F.Bits{xl, xh}), LT{}, GT{}))))) : Bool}:
305  match bad z:
306    case True{} _:
307      {==}
308    case False{} True{}:
309      {==}
310    case False{} False{}:
311      +nx = or_l(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh}), hbad)
312      +ny = or_r(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh}), hbad)
313      +e1 = Equal.trans(Bool, F.lt_s(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), F.lt_s(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), F.lt_s(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), Equal.cong(Bool, Bool, t => F.lt_s(F.Bits{xl, xh}, F.Bits{yl, yh}, t, F.signbit(F.Bits{yl, yh})), F.signbit(F.Bits{xl, xh}), SF.sign(F.Bits{xl, xh}), FB.signbit_value(F.Bits{xl, xh})), Equal.cong(Bool, Bool, t => F.lt_s(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t), F.signbit(F.Bits{yl, yh}), SF.sign(F.Bits{yl, yh}), FB.signbit_value(F.Bits{yl, yh})))
314      Equal.trans(Bool, F.lt_s(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), F.lt_s(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), Cmp.is_lt(SF.pick(Cmp, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), SF.pick(Cmp, SF.sign(F.Bits{xl, xh}), SF.flip(SF.mag_cmp(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.mag_cmp(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.pick(Cmp, SF.sign(F.Bits{xl, xh}), LT{}, GT{}))), e1, lts(xl, xh, yl, yh, SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), SF.mag_cmp(F.Bits{xl, xh}, F.Bits{yl, yh}), hm(one, h1, xl, xh, yl, yh, nx, ny), hm2(one, h1, xl, xh, yl, yh, nx, ny)))