F64round.ovle: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as F64round Lines 599-607 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&start_line=599&end_line=607 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/w64.bend as SW import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD # SoftFloat's carry test: 2^63 <= sig + 2^9 def ovle(+one: Nat, +h1: {one == 1n : Nat}, +sig: WU.U64, +hS: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {X.le(WU.U64{0, c}, X.add(sig, WU.U64{512, 0})) == Bool.not(C.fits(63n, Nat.add(SW.value(sig), 512n))) : Bool}: a1 = WA.add_value(sig, WU.U64{512, 0}) +ev1 = Equal.trans(Nat, SW.value(X.add(sig, WU.U64{512, 0})), C.low(64n, Nat.add(SW.value(sig), 512n)), Nat.add(SW.value(sig), 512n), a1, WW.low_fit(64n, Nat.add(SW.value(sig), 512n), fits_add1(63n, SW.value(sig), 512n, hS, {==}))) +ec = Equal.trans(Nat, C.shift(32n, v(c)), C.shift(32n, C.shift(31n, one)), C.shift(63n, one), Equal.cong(Nat, Nat, z => C.shift(32n, z), v(c), C.shift(31n, one), FB.pwv(31n, {==}, one, h1, c, hc)), Equal.sym(Nat, C.shift(63n, one), C.shift(32n, C.shift(31n, one)), WW.shift_comp(32n, 31n, one))) l1 = WA.lt_value(X.add(sig, WU.U64{512, 0}), WU.U64{0, c}) +e2 = Equal.trans(Bool, Nat.is_lt(SW.value(X.add(sig, WU.U64{512, 0})), C.shift(32n, v(c))), Nat.is_lt(Nat.add(SW.value(sig), 512n), C.shift(32n, v(c))), Nat.is_lt(Nat.add(SW.value(sig), 512n), C.shift(63n, one)), Equal.cong(Nat, Bool, z => Nat.is_lt(z, C.shift(32n, v(c))), SW.value(X.add(sig, WU.U64{512, 0})), Nat.add(SW.value(sig), 512n), ev1), Equal.cong(Nat, Bool, z => Nat.is_lt(Nat.add(SW.value(sig), 512n), z), C.shift(32n, v(c)), C.shift(63n, one), ec)) +e3 = Equal.trans(Bool, X.lt(X.add(sig, WU.U64{512, 0}), WU.U64{0, c}), Nat.is_lt(Nat.add(SW.value(sig), 512n), C.shift(63n, one)), C.fits(63n, Nat.add(SW.value(sig), 512n)), Equal.trans(Bool, X.lt(X.add(sig, WU.U64{512, 0}), WU.U64{0, c}), Nat.is_lt(SW.value(X.add(sig, WU.U64{512, 0})), C.shift(32n, v(c))), Nat.is_lt(Nat.add(SW.value(sig), 512n), C.shift(63n, one)), l1, e2), lt_fit(63n, one, h1, Nat.add(SW.value(sig), 512n))) Equal.cong(Bool, Bool, t => Bool.not(t), X.lt(X.add(sig, WU.U64{512, 0}), WU.U64{0, c}), C.fits(63n, Nat.add(SW.value(sig), 512n)), e3) Uses (26): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=pw https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=pwv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=fits_add1 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=lt_fit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=add_value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=lt_value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fit https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_comp https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=lt