W64sqrt.up: def of bend-collections-laws-math@1.0.0.0 Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64sqrt Lines 180-201 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&start_line=180&end_line=201 import Base 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/lib/u32.bend as U import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD def up(+fu: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: U32, +r: U32, +m: U32, +pm: {m == U32{WD.mask(32n, 16n)} : U32}, +hf: {Nat.is_lt(Nat.sub(v(m), v(r)), fu) == True{} : Bool}, +hle: {Nat.is_le(v(r), v(m)) == True{} : Bool}, +hs: {Nat.is_le(sq(v(r)), v(x)) == True{} : Bool}, +ub: Bool, +hub: {up_okg(x, r, m) == ub : Bool}) -> {Nat.is_le(sq(v(up32g(fu, x, r, ub, m))), v(x)) == True{} : Bool} & {Nat.is_lt(v(x), sq(1n+v(up32g(fu, x, r, ub, m)))) == True{} : Bool}: match fu: case 0n: Empty.absurd({Nat.is_le(sq(v(up32g(0n, x, r, ub, m))), v(x)) == True{} : Bool} & {Nat.is_lt(v(x), sq(1n+v(up32g(0n, x, r, ub, m)))) == True{} : Bool}, N.lt_zero_absurd(Nat.sub(v(m), v(r)), hf)) case 1n+ +g: match ub: case False{}: (hs, up_stop(one, h1, x, r, m, pm, hle, U32.is_le(U32.mul(U32.add(r, 1), U32.add(r, 1)), x), {==}, U32.is_lt(r, m), {==}, hub)) case True{}: +r1 = U32.add(r, 1) +ha = and_l(U32.is_lt(r, m), U32.is_le(U32.mul(r1, r1), x), hub) +hb = and_r(U32.is_lt(r, m), U32.is_le(U32.mul(r1, r1), x), hub) +lt = Equal.trans(Bool, Nat.is_lt(v(r), v(m)), U32.is_lt(r, m), True{}, Equal.sym(Bool, U32.is_lt(r, m), Nat.is_lt(v(r), v(m)), U.is_lt_nat(r, m)), ha) +e1 = succ_v(one, h1, r, m, pm, lt) +em = m16(one, h1, m, pm) +bs1 = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(16n, one)) == True{} : Bool}, 1n+v(r), v(r1), Equal.sym(Nat, v(r1), 1n+v(r), e1), N.le_lt_trans(1n+v(r), v(m), WD.sc(16n, one), lt_to_le(v(r), v(m), lt), L.subst(Nat, z => {Nat.is_lt(v(m), z) == True{} : Bool}, 1n+v(m), WD.sc(16n, one), em, N.lt_succ(v(m))))) +esq = sq_exact(one, h1, r1, bs1) +hs1 = L.subst(Nat, z => {Nat.is_le(z, v(x)) == True{} : Bool}, v(U32.mul(r1, r1)), sq(v(r1)), esq, Equal.trans(Bool, Nat.is_le(v(U32.mul(r1, r1)), v(x)), U32.is_le(U32.mul(r1, r1), x), True{}, Equal.sym(Bool, U32.is_le(U32.mul(r1, r1), x), Nat.is_le(v(U32.mul(r1, r1)), v(x)), is_le_nat(U32.mul(r1, r1), x)), hb)) +hle1 = L.subst(Nat, z => {Nat.is_le(z, v(m)) == True{} : Bool}, 1n+v(r), v(r1), Equal.sym(Nat, v(r1), 1n+v(r), e1), lt_to_le(v(r), v(m), lt)) +hf0 = L.subst(Nat, z => {Nat.is_lt(z, 1n+g) == True{} : Bool}, Nat.sub(v(m), v(r)), 1n+Nat.sub(v(m), 1n+v(r)), sub_succ_r(v(r), v(m), lt), hf) +hf1 = L.subst(Nat, z => {Nat.is_lt(Nat.sub(v(m), z), g) == True{} : Bool}, 1n+v(r), v(r1), Equal.sym(Nat, v(r1), 1n+v(r), e1), hf0) up(g, one, h1, x, r1, m, pm, hf1, hle1, hs1, up_okg(x, r1, m), {==}) Uses (35): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd 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.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=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul 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=le_lt_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_succ https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_zero_absurd https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend&name=is_lt_nat https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=mask https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=and_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=and_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=is_le_nat https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=lt_to_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=m16 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=sq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=sq_exact https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=sub_succ_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=succ_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=up32g https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=up_okg https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=up_stop https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend&name=v