def eqs

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

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/proofs/lib/u32.bend as U

293def eqs(+eL: Bool, +eW: Bool, +sa: Bool, +sb: Bool, +mc: Cmp, +h: {Bool.and(eL, eW) == Cmp.is_eq(mc) : Bool}) -> {Bool.and(eL, Bool.and(eW, Nat.is_eq(SF.b2n(sa), SF.b2n(sb)))) == Cmp.is_eq(SF.pick(Cmp, Bool.not(Bool.xor(sa, sb)), SF.pick(Cmp, sa, SF.flip(mc), mc), SF.pick(Cmp, sa, LT{}, GT{}))) : Bool}:
294  match sa sb:
295    case True{} True{}:
296      Equal.trans(Bool, Bool.and(eL, Bool.and(eW, True{})), Bool.and(eL, eW), Cmp.is_eq(SF.flip(mc)), Equal.cong(Bool, Bool, t => Bool.and(eL, t), Bool.and(eW, True{}), eW, U.and_true(eW)), Equal.trans(Bool, Bool.and(eL, eW), Cmp.is_eq(mc), Cmp.is_eq(SF.flip(mc)), h, eqflip(mc)))
297    case False{} False{}:
298      Equal.trans(Bool, Bool.and(eL, Bool.and(eW, True{})), Bool.and(eL, eW), Cmp.is_eq(mc), Equal.cong(Bool, Bool, t => Bool.and(eL, t), Bool.and(eW, True{}), eW, U.and_true(eW)), h)
299    case True{} False{}:
300      andff(eL, eW)
301    case False{} True{}:
302      andff(eL, eW)