def le_value

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

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

362def le_value(+x: F.F64, +y: F.F64) -> SF.Le.value(x, y):
363  match x y:
364    case F.Bits{+xl, +xh} F.Bits{+yl, +yh}:
365      +ebad = Equal.trans(Bool, Bool.or(F.is_nan(F.Bits{xl, xh}), F.is_nan(F.Bits{yl, yh})), Bool.or(SF.is_nan(F.Bits{xl, xh}), F.is_nan(F.Bits{yl, yh})), Bool.or(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh})), Equal.cong(Bool, Bool, t => Bool.or(t, F.is_nan(F.Bits{yl, yh})), F.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{xl, xh}), FB.is_nan_value(F.Bits{xl, xh})), Equal.cong(Bool, Bool, t => Bool.or(SF.is_nan(F.Bits{xl, xh}), t), F.is_nan(F.Bits{yl, yh}), SF.is_nan(F.Bits{yl, yh}), FB.is_nan_value(F.Bits{yl, yh})))
366      +ez = Equal.trans(Bool, Bool.and(F.is_zero(F.Bits{xl, xh}), F.is_zero(F.Bits{yl, yh})), Bool.and(SF.is_zero(F.Bits{xl, xh}), F.is_zero(F.Bits{yl, yh})), Bool.and(SF.is_zero(F.Bits{xl, xh}), SF.is_zero(F.Bits{yl, yh})), Equal.cong(Bool, Bool, t => Bool.and(t, F.is_zero(F.Bits{yl, yh})), F.is_zero(F.Bits{xl, xh}), SF.is_zero(F.Bits{xl, xh}), FB.is_zero_value(F.Bits{xl, xh})), Equal.cong(Bool, Bool, t => Bool.and(SF.is_zero(F.Bits{xl, xh}), t), F.is_zero(F.Bits{yl, yh}), SF.is_zero(F.Bits{yl, yh}), FB.is_zero_value(F.Bits{yl, yh})))
367      +e1 = Equal.trans(Bool, F.le_z(F.Bits{xl, xh}, F.Bits{yl, yh}, Bool.or(F.is_nan(F.Bits{xl, xh}), F.is_nan(F.Bits{yl, yh})), Bool.and(F.is_zero(F.Bits{xl, xh}), F.is_zero(F.Bits{yl, yh}))), F.le_z(F.Bits{xl, xh}, F.Bits{yl, yh}, Bool.or(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh})), Bool.and(F.is_zero(F.Bits{xl, xh}), F.is_zero(F.Bits{yl, yh}))), F.le_z(F.Bits{xl, xh}, F.Bits{yl, yh}, Bool.or(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh})), Bool.and(SF.is_zero(F.Bits{xl, xh}), SF.is_zero(F.Bits{yl, yh}))), Equal.cong(Bool, Bool, t => F.le_z(F.Bits{xl, xh}, F.Bits{yl, yh}, t, Bool.and(F.is_zero(F.Bits{xl, xh}), F.is_zero(F.Bits{yl, yh}))), Bool.or(F.is_nan(F.Bits{xl, xh}), F.is_nan(F.Bits{yl, yh})), Bool.or(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh})), ebad), Equal.cong(Bool, Bool, t => F.le_z(F.Bits{xl, xh}, F.Bits{yl, yh}, Bool.or(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh})), t), Bool.and(F.is_zero(F.Bits{xl, xh}), F.is_zero(F.Bits{yl, yh})), Bool.and(SF.is_zero(F.Bits{xl, xh}), SF.is_zero(F.Bits{yl, yh})), ez))
368      Equal.trans(Bool, F.le_z(F.Bits{xl, xh}, F.Bits{yl, yh}, Bool.or(F.is_nan(F.Bits{xl, xh}), F.is_nan(F.Bits{yl, yh})), Bool.and(F.is_zero(F.Bits{xl, xh}), F.is_zero(F.Bits{yl, yh}))), F.le_z(F.Bits{xl, xh}, F.Bits{yl, yh}, Bool.or(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh})), Bool.and(SF.is_zero(F.Bits{xl, xh}), SF.is_zero(F.Bits{yl, yh}))), Bool.and(Bool.not(Bool.or(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh}))), Cmp.is_le(SF.pick(Cmp, Bool.and(SF.is_zero(F.Bits{xl, xh}), SF.is_zero(F.Bits{yl, yh})), 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{}))))), e1, le_gen(1n, {==}, xl, xh, yl, yh, Bool.or(SF.is_nan(F.Bits{xl, xh}), SF.is_nan(F.Bits{yl, yh})), {==}, Bool.and(SF.is_zero(F.Bits{xl, xh}), SF.is_zero(F.Bits{yl, yh}))))