def rca

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addg.bend:118

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/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

118def rca(+s: Bool, +a: Nat, +a2: Nat, +ha: {a == a2 : Nat}, +k: Nat, +k2: Nat, +hk: {k == k2 : Nat}, +m: Nat, +m2: Nat, +hm: {m == m2 : Nat}, +x: Nat, +x2: Nat, +hx: {x == x2 : Nat}) -> {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(a2, C.shift(k2, m2)), x2) : F.F64}:
119  +e1 = L.subst(Nat, z => {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(z, C.shift(k, m)), x) : F.F64}, a, a2, ha, {==})
120  +e2 = L.subst(Nat, z => {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(a2, C.shift(z, m)), x) : F.F64}, k, k2, hk, e1)
121  +e3 = L.subst(Nat, z => {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(a2, C.shift(k2, z)), x) : F.F64}, m, m2, hm, e2)
122  L.subst(Nat, z => {SF.round(s, Nat.add(a, C.shift(k, m)), x) == SF.round(s, Nat.add(a2, C.shift(k2, m2)), z) : F.F64}, x, x2, hx, e3)