def spec_eq

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

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/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend as AG

109def spec_eq(+sa: Bool, +sb: Bool, +ea: Nat, +Fa: Nat, +Fb: Nat) -> {SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(ea))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(ea))), AG.mt(ea, Fb)), Nat.min(AG.xe(ea), AG.xe(ea))) == SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)) : F.F64}:
110  +e1 = Equal.cong(Nat, F.F64, w => SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), w), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(ea), w), AG.mt(ea, Fb)), w), Nat.min(AG.xe(ea), AG.xe(ea)), AG.xe(ea), AG.min_l(AG.xe(ea), AG.xe(ea), N.le_refl(AG.xe(ea))))
111  +e2 = Equal.cong(Nat, F.F64, z => SF.add_mag(sa, C.shift(z, AG.mt(ea, Fa)), sb, C.shift(z, AG.mt(ea, Fb)), AG.xe(ea)), Nat.sub(AG.xe(ea), AG.xe(ea)), 0n, N.sub_self(AG.xe(ea)))
112  +e3 = Equal.trans(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(ea)), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(ea), AG.xe(ea)), AG.mt(ea, Fb)), AG.xe(ea)), SF.add_mag(sa, C.shift(0n, AG.mt(ea, Fa)), sb, C.shift(0n, AG.mt(ea, Fb)), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), e2, Equal.cong(F.F64, F.F64, zz_ => zz_, SF.add_mag(sa, C.shift(0n, AG.mt(ea, Fa)), sb, C.shift(0n, AG.mt(ea, Fb)), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), {==}))
113  Equal.trans(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(ea))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(ea))), AG.mt(ea, Fb)), Nat.min(AG.xe(ea), AG.xe(ea))), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(ea)), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(ea), AG.xe(ea)), AG.mt(ea, Fb)), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), e1, e3)