def spec_gt

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

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

103def spec_gt(+sa: Bool, +sb: Bool, +ea: Nat, +eb: Nat, +Fa: Nat, +Fb: Nat, +h: {Nat.is_le(AG.xe(eb), AG.xe(ea)) == True{} : Bool}) -> {SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(eb, Fb)), Nat.min(AG.xe(ea), AG.xe(eb))) == SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)) : F.F64}:
104  +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(eb), w), AG.mt(eb, Fb)), w), Nat.min(AG.xe(ea), AG.xe(eb)), AG.xe(eb), AG.min_r(AG.xe(ea), AG.xe(eb), h))
105  +e2 = Equal.cong(Nat, F.F64, z => SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, C.shift(z, AG.mt(eb, Fb)), AG.xe(eb)), Nat.sub(AG.xe(eb), AG.xe(eb)), 0n, N.sub_self(AG.xe(eb)))
106  +e3 = Equal.trans(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(eb)), AG.mt(eb, Fb)), AG.xe(eb)), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, C.shift(0n, AG.mt(eb, Fb)), AG.xe(eb)), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), e2, Equal.cong(Nat, F.F64, zz_ => SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, zz_, AG.xe(eb)), C.shift(0n, AG.mt(eb, Fb)), AG.mt(eb, Fb), {==}))
107  Equal.trans(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(eb, Fb)), Nat.min(AG.xe(ea), AG.xe(eb))), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(eb)), AG.mt(eb, Fb)), AG.xe(eb)), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), e1, e3)