def rmp_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:569

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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

569def rmp_c(+s: Bool, +u: Nat, +hu: {Nat.is_le(63n, u) == True{} : Bool}, +b: WU.U64, +r: WU.U64, +Bv: Nat, +Rv: Nat, +eb: {SW.value(b) == Bv : Nat}, +er: {SW.value(r) == Rv : Nat}, +hRB: {Nat.is_le(Rv, Bv) == True{} : Bool}, +c: Bool) -> {F.rm_pick(s, u, b, r, c) == SF.pick(F.F64, c, SF.round(Bool.not(s), Nat.sub(Bv, Rv), u), SF.round(s, Rv, u)) : F.F64}:
570  match c:
571    case True{}:
572      +hle = L.subst(Nat, t => {Nat.is_le(t, SW.value(b)) == True{} : Bool}, Rv, SW.value(r), Equal.sym(Nat, SW.value(r), Rv, er), L.subst(Nat, t => {Nat.is_le(Rv, t) == True{} : Bool}, Bv, SW.value(b), Equal.sym(Nat, SW.value(b), Bv, eb), hRB))
573      +es = Equal.trans(Nat, SW.value(X.sub(b, r)), Nat.sub(SW.value(b), SW.value(r)), Nat.sub(Bv, Rv), WA.sub_value(b, r, hle), Equal.trans(Nat, Nat.sub(SW.value(b), SW.value(r)), Nat.sub(Bv, SW.value(r)), Nat.sub(Bv, Rv), Equal.cong(Nat, Nat, t => Nat.sub(t, SW.value(r)), SW.value(b), Bv, eb), Equal.cong(Nat, Nat, t => Nat.sub(Bv, t), SW.value(r), Rv, er)))
574      Equal.trans(F.F64, F.round_w(Bool.not(s), u, X.sub(b, r)), SF.round(Bool.not(s), SW.value(X.sub(b, r)), u), SF.round(Bool.not(s), Nat.sub(Bv, Rv), u), T.rw_value(Bool.not(s), u, X.sub(b, r), hu), Equal.cong(Nat, F.F64, t => SF.round(Bool.not(s), t, u), SW.value(X.sub(b, r)), Nat.sub(Bv, Rv), es))
575    case False{}:
576      Equal.trans(F.F64, F.round_w(s, u, r), SF.round(s, SW.value(r), u), SF.round(s, Rv, u), T.rw_value(s, u, r, hu), Equal.cong(Nat, F.F64, t => SF.round(s, t, u), SW.value(r), Rv, er))