def rcs

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

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

124def rcs(+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.sub(C.shift(k, m), a), x) == SF.round(s, Nat.sub(C.shift(k2, m2), a2), x2) : F.F64}:
125  +e1 = L.subst(Nat, z => {SF.round(s, Nat.sub(C.shift(k, m), a), x) == SF.round(s, Nat.sub(C.shift(k, m), z), x) : F.F64}, a, a2, ha, {==})
126  +e2 = L.subst(Nat, z => {SF.round(s, Nat.sub(C.shift(k, m), a), x) == SF.round(s, Nat.sub(C.shift(z, m), a2), x) : F.F64}, k, k2, hk, e1)
127  +e3 = L.subst(Nat, z => {SF.round(s, Nat.sub(C.shift(k, m), a), x) == SF.round(s, Nat.sub(C.shift(k2, z), a2), x) : F.F64}, m, m2, hm, e2)
128  L.subst(Nat, z => {SF.round(s, Nat.sub(C.shift(k, m), a), x) == SF.round(s, Nat.sub(C.shift(k2, m2), a2), z) : F.F64}, x, x2, hx, e3)