W64est.yv: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend as W64est Lines 125-148 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend&start_line=125&end_line=148 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/lib/nat.bend as N import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dm.bend as DM 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/w64sh.bend as SH import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW # x >> t as the sum of xl >> t and xh << (64 - t), below 2^64 def yv(+xl: WU.U64, +xh: U32, +t: Nat, +t1: {Nat.is_le(1n, t) == True{} : Bool}, +t32: {Nat.is_le(t, 32n) == True{} : Bool}, +hx: {C.fits(Nat.add(64n, t), DM.X96(xl, xh)) == True{} : Bool}) -> {SW.value(X.add(X.shr(xl, t), X.shl(WU.U64{xh, 0}, Nat.sub(64n, t)))) == C.high(t, DM.X96(xl, xh)) : Nat}: +k = Nat.sub(64n, t) +x9 = DM.X96(xl, xh) +t64 = N.le_trans(t, 32n, 64n, t32, {==}) +ek = N.sub_add(64n, t, t64) +h64 = Equal.trans(Bool, Nat.is_lt(Nat.add(64n, 0n), Nat.add(64n, t)), Nat.is_lt(0n, t), True{}, WW.lt_cancel_l(64n, 0n, t), N.succ_le_lt(0n, t, t1)) +hk = N.sub_lt(64n, t, 64n, t64, L.subst(Nat, z => {Nat.is_lt(64n, z) == True{} : Bool}, Nat.add(64n, t), Nat.add(t, 64n), N.add_comm(64n, t), h64)) +exh = WW.high_u(64n, SW.value(xl), v(xh), DM.fit64(xl)) +fxh = L.subst(Nat, z => {C.fits(t, z) == True{} : Bool}, C.high(64n, x9), v(xh), exh, SH.fits_high(64n, t, x9, hx)) +s = C.shift(k, v(xh)) +eka = Equal.trans(Nat, Nat.add(k, t), Nat.add(t, k), 64n, N.add_comm(k, t), ek) +hs0 = WW.shift_lt(k, v(xh), C.pow2(t), WW.lt_of_fits(t, v(xh), fxh)) +els = low_shift(64n, k, t, v(xh), eka, hs0) +esh = Equal.trans(Nat, C.shift(64n, v(xh)), C.shift(Nat.add(t, k), v(xh)), C.shift(t, s), Equal.cong(Nat, Nat, z => C.shift(z, v(xh)), 64n, Nat.add(t, k), Equal.sym(Nat, Nat.add(t, k), 64n, ek)), WW.shift_comp(t, k, v(xh))) +ex = Equal.cong(Nat, Nat, z => Nat.add(SW.value(xl), z), C.shift(64n, v(xh)), C.shift(t, s), esh) +ehx = Equal.trans(Nat, C.high(t, x9), C.high(t, Nat.add(SW.value(xl), C.shift(t, s))), Nat.add(C.high(t, SW.value(xl)), s), Equal.cong(Nat, Nat, z => C.high(t, z), x9, Nat.add(SW.value(xl), C.shift(t, s)), ex), WW.high_add_shift(t, SW.value(xl), s)) +hx2 = L.subst(Nat, z => {C.fits(z, x9) == True{} : Bool}, Nat.add(64n, t), Nat.add(t, 64n), N.add_comm(64n, t), hx) +fy = SH.fits_high(t, 64n, x9, hx2) +a = X.shr(xl, t) +bw = X.shl(WU.U64{xh, 0}, k) +eb = Equal.trans(Nat, SW.value(bw), C.low(64n, C.shift(k, SW.value(WU.U64{xh, 0}))), s, SH.shl_value(WU.U64{xh, 0}, k, hk), Equal.trans(Nat, C.low(64n, C.shift(k, SW.value(WU.U64{xh, 0}))), C.low(64n, s), s, Equal.cong(Nat, Nat, z => C.low(64n, C.shift(k, z)), SW.value(WU.U64{xh, 0}), v(xh), DM.u32_0(xh)), els)) +esum = Equal.trans(Nat, Nat.add(SW.value(a), SW.value(bw)), Nat.add(C.high(t, SW.value(xl)), s), C.high(t, x9), Equal.trans(Nat, Nat.add(SW.value(a), SW.value(bw)), Nat.add(C.high(t, SW.value(xl)), SW.value(bw)), Nat.add(C.high(t, SW.value(xl)), s), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(bw)), SW.value(a), C.high(t, SW.value(xl)), SH.shr_value(xl, t)), Equal.cong(Nat, Nat, z => Nat.add(C.high(t, SW.value(xl)), z), SW.value(bw), s, eb)), Equal.sym(Nat, C.high(t, x9), Nat.add(C.high(t, SW.value(xl)), s), ehx)) Equal.trans(Nat, SW.value(X.add(a, bw)), C.low(64n, Nat.add(SW.value(a), SW.value(bw))), C.high(t, x9), WA.add_value(a, bw), Equal.trans(Nat, C.low(64n, Nat.add(SW.value(a), SW.value(bw))), C.low(64n, C.high(t, x9)), C.high(t, x9), Equal.cong(Nat, Nat, z => C.low(64n, z), Nat.add(SW.value(a), SW.value(bw)), C.high(t, x9), esum), WW.low_fit(64n, C.high(t, x9), fy))) Uses (42): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool 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_le 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=Nat.sub 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/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=succ_le_lt 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/w64dm.bend&name=X96 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dm.bend&name=fit64 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dm.bend&name=u32_0 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend&name=low_shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64est.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=fits_high https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=shl_value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=shr_value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=high_add_shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=high_u 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=lt_cancel_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=lt_of_fits 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/proofs/math/typed/width.bend&name=shift_lt 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=high 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=pow2 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=shl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=shr