U32int.subv: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend as U32int Lines 527-542 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend&start_line=527&end_line=542 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/src/math/generic.bend as G import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I 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/u32laws.bend as LW import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF def subv(+k: Nat, +hk: {k == 32n : Nat}, +m: U32, +mp: Nat, +hm: {v(m) == 1n+mp : Nat}, +s0: U32, +x: U32, +ns0: Nat, +nx: Nat, +hs0: {v(s0) == ns0 : Nat}, +hx: {v(x) == nx : Nat}, +hb0: {Nat.is_lt(ns0, 1n+mp) == True{} : Bool}, +hbx: {Nat.is_lt(nx, 1n+mp) == True{} : Bool}, +c: Bool, +hc: {I.u32_is(NM.Lt{s0, x}) == c : Bool}) -> {v(G.submod(~U32, ~I.u32_op, m, s0, x, c)) == Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp) : Nat}: match c: case True{}: +hl = Equal.trans(Bool, Nat.is_lt(ns0, nx), I.u32_is(NM.Lt{s0, x}), True{}, Equal.sym(Bool, I.u32_is(NM.Lt{s0, x}), Nat.is_lt(ns0, nx), ltv(s0, x, ns0, nx, hs0, hx)), hc) +y = I.u32_op(NM.Sub{m, x}) +ey = Equal.trans(Nat, v(y), Nat.sub(v(m), v(x)), Nat.sub(1n+mp, nx), LW.ops_sub(m, x, N.lt_le(v(x), v(m), lt_mn(x, m, mp, hm, nx, hx, hbx))), nsub(v(m), v(x), 1n+mp, nx, hm, hx)) +sum = Nat.add(ns0, Nat.sub(1n+mp, nx)) +hsum = NF.sm_lt(1n+mp, ns0, nx, hl, N.lt_le(nx, 1n+mp, hbx)) +esum = nadd(v(s0), v(y), ns0, Nat.sub(1n+mp, nx), hs0, ey) +hfit = fits32(k, hk, Nat.add(v(s0), v(y)), L.subst(Nat, z => {Nat.is_lt(z, C.pow2(k)) == True{} : Bool}, sum, Nat.add(v(s0), v(y)), Equal.sym(Nat, Nat.add(v(s0), v(y)), sum, esum), N.lt_trans(sum, 1n+mp, C.pow2(k), hsum, mv(k, hk, m, mp, hm)))) +hao = Equal.trans(Bool, I.u32_is(NM.AddOver{s0, y}), Bool.not(C.fits(32n, Nat.add(v(s0), v(y)))), False{}, LW.tests_add_over(s0, y), Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(32n, Nat.add(v(s0), v(y))), True{}, hfit)) Equal.trans(Nat, v(I.u32_op(NM.Add{s0, y})), Nat.add(v(s0), v(y)), Nat.mod(sum, 1n+mp), LW.ops_add(s0, y, hao), Equal.trans(Nat, Nat.add(v(s0), v(y)), sum, Nat.mod(sum, 1n+mp), esum, Equal.sym(Nat, Nat.mod(sum, 1n+mp), sum, NF.mod_small(mp, sum, hsum)))) case False{}: +hl = Equal.trans(Bool, Nat.is_lt(ns0, nx), I.u32_is(NM.Lt{s0, x}), False{}, Equal.sym(Bool, I.u32_is(NM.Lt{s0, x}), Nat.is_lt(ns0, nx), ltv(s0, x, ns0, nx, hs0, hx)), hc) +hlv = Equal.trans(Bool, Nat.is_lt(v(s0), v(x)), I.u32_is(NM.Lt{s0, x}), False{}, Equal.sym(Bool, I.u32_is(NM.Lt{s0, x}), Nat.is_lt(v(s0), v(x)), LW.tests_lt(s0, x)), hc) Equal.trans(Nat, v(I.u32_op(NM.Sub{s0, x})), Nat.sub(v(s0), v(x)), Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp), LW.ops_sub(s0, x, N.not_lt_le(v(s0), v(x), hlv)), Equal.trans(Nat, Nat.sub(v(s0), v(x)), Nat.sub(ns0, nx), Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp), nsub(v(s0), v(x), ns0, nx, hs0, hx), Equal.sym(Nat, Nat.mod(Nat.add(ns0, Nat.sub(1n+mp, nx)), 1n+mp), Nat.sub(ns0, nx), NF.sm_ge(mp, ns0, nx, N.not_lt_le(ns0, nx, hl), hb0)))) Uses (36): 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=Nat.mod 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=lt_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=not_lt_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend&name=mod_small https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend&name=sm_ge https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend&name=sm_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend&name=fits32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend&name=lt_mn https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend&name=ltv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend&name=mv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend&name=nadd https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend&name=nsub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend&name=ops_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend&name=ops_sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend&name=tests_add_over https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend&name=tests_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=pow2 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/generic.bend&name=submod https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/instances.bend&name=u32_is https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/instances.bend&name=u32_op https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/num.bend&name=Op https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/num.bend&name=Test