def ar_c

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

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/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NE
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

147def ar_c(+x: F.F64, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {SF.rtriple(F.ar_cls(x, t)) == SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, Bool.and(t, Bool.not(z)), Fail{NE.BadDomain{}}, SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, Bool.and(t, z), Fail{NE.Overflow{}}, SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, SF.is_zero(x), Done{SF.Rat{False{}, 0n, 0n}}, FINR(x, Nat.is_le(SF.zb(), SF.xexp(x)))))) : Result<&2, &2, NE.NumError, SF.Rat>}:
148  match t z:
149    case True{} True{}:
150      Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, b => SF.rtriple(F.ar_top(Bool.not(b))), X.is_zero(F.frac(x)), True{}, hz)
151    case True{} False{}:
152      Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, b => SF.rtriple(F.ar_top(Bool.not(b))), X.is_zero(F.frac(x)), False{}, hz)
153    case False{} _:
154      +e1 = Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, b => SF.rtriple(F.ar_z(x, b)), F.is_zero(x), SF.is_zero(x), FB.is_zero_value(x))
155      Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, SF.rtriple(F.ar_z(x, F.is_zero(x))), SF.rtriple(F.ar_z(x, SF.is_zero(x))), SF.pick(Result<&2, &2, NE.NumError, SF.Rat>, SF.is_zero(x), Done{SF.Rat{False{}, 0n, 0n}}, FINR(x, Nat.is_le(SF.zb(), SF.xexp(x)))), e1, arz_c(x, SF.is_zero(x)))