def ab_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64ratio.bend:79

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/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/src/math/num.bend as NE
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
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/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64nrp.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as BL

79def ab_c(+s: Bool, +w: WU.U64, +k: Nat, +hz: {Nat.is_eq(SW.value(w), 0n) == False{} : Bool}, +c: Bool, +hc: {Nat.is_le(Nat.add(k, M.bit_length(SW.value(w))), 64n) == c : Bool}) -> {SF.rtriple(F.ar_big(s, w, k, c)) == BIGR(s, C.shift(k, SW.value(w))) : Result<&2, &2, NE.NumError, SF.Rat>}:
80  match c:
81    case True{}:
82      +V = SW.value(w)
83      +B = M.bit_length(V)
84      +S = C.shift(k, V)
85      +hb1 = BL.bl_pos(V, hz, B, {==})
86      +hkl = Equal.trans(Bool, Nat.is_lt(k, Nat.add(k, B)), Nat.is_lt(Nat.add(k, 0n), Nat.add(k, B)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, Nat.add(k, B)), k, Nat.add(k, 0n), Equal.sym(Nat, Nat.add(k, 0n), k, N.add_zero(k))), N.lt_add_left(0n, B, k, N.succ_le_lt(0n, B, hb1)))
87      +hk = N.lt_le_trans(k, Nat.add(k, B), 64n, hkl, hc)
88      +ev = FL.shl_v(w, k, B, hk, hc, RT.bl_fit(V))
89      +hf = SH.fits_mono(Nat.add(k, B), 64n, S, hc, NR.tbf(k, V, Nat.add(k, B), {==}))
90      +e1 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, n => Done{SF.Rat{s, n, 0n}}, SW.value(X.shl(w, k)), S, ev)
91      +e2 = Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, b => SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, b, Done{SF.Rat{s, S, 0n}}, Fail{NE.Overflow{}}), C.fits(64n, S), True{}, hf)
92      Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, Done{SF.Rat{s, SW.value(X.shl(w, k)), 0n}}, Done{SF.Rat{s, S, 0n}}, BIGR(s, S), e1, Equal.sym(Result<&2, &2, NE.NumError, SF.Rat>, BIGR(s, S), Done{SF.Rat{s, S, 0n}}, e2))
93    case False{}:
94      +V = SW.value(w)
95      +B = M.bit_length(V)
96      +S = C.shift(k, V)
97      +J = Nat.add(k, B)
98      +K = Nat.sub(J, 1n)
99      +hJ = N.not_le_lt(J, 64n, hc)
100      +hJ1 = N.le_trans(1n, 65n, J, {==}, N.lt_succ_le_succ(64n, J, hJ))
101      +ek = Equal.sym(Nat, Nat.add(1n, K), J, N.sub_add(J, 1n, hJ1))
102      +hK = N.lt_succ_le(64n, K, L.subst(Nat, t => {Nat.is_lt(64n, t) == True{} : Bool}, J, 1n+K, ek, hJ))
103      +nf = FL.nfit_mono(64n, K, S, hK, NR.tbn(k, V, K, hz, ek))
104      Equal.sym(Result<&2, &2, NE.NumError, SF.Rat>, BIGR(s, S), Fail{NE.Overflow{}}, Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, b => SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, b, Done{SF.Rat{s, S, 0n}}, Fail{NE.Overflow{}}), C.fits(64n, S), False{}, nf))