def rc2

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addf.bend:92

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/lib/logic.bend as L

92def rc2(+s: Bool, +s2: Bool, +hs: {s == s2 : Bool}, +m: Nat, +m2: Nat, +hm: {m == m2 : Nat}, +x: Nat, +x2: Nat, +hx: {x == x2 : Nat}) -> {SF.round(s, m, x) == SF.round(s2, m2, x2) : F.F64}:
93  +e1 = L.subst(Bool, z => {SF.round(s, m, x) == SF.round(z, m, x) : F.F64}, s, s2, hs, {==})
94  +e2 = L.subst(Nat, z => {SF.round(s, m, x) == SF.round(s2, z, x) : F.F64}, m, m2, hm, e1)
95  L.subst(Nat, z => {SF.round(s, m, x) == SF.round(s2, m2, z) : F.F64}, x, x2, hx, e2)