PROOF.ud.fin: def of bend-osdev-u32@0.1.0.0 Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF Lines 1763-1768 of bend-osdev-u32@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&start_line=1763&end_line=1768 import Base import bend-osdev-u32@0.1.0.0/u32.bend as U import bend-osdev-u32@0.1.0.0/LAWS.bend as Laws def ud.fin(+p: Nat, +q: Word(p), +s: Word(32n), +bw: Word(32n), +T: Bool, +g: Bool, +a0: Bool, +rw: Word(32n), +x: Nat, +x2: Nat, +eg: {Bool.or(T, U32.is_ge(U32{s}, U32{bw})) == g : Bool}, +eput: {Nat.add(Word.to_nat(32n, s), U.U32Nat.dbl(32n, U.U32Nat.bit(T))) == Nat.add(U.U32Nat.bit(a0), Nat.double(Word.to_nat(32n, rw))) : Nat}, +ex: {Nat.add(U.U32Nat.bit(a0), Nat.double(x)) == x2 : Nat}, +i1: {Nat.add(Nat.mul(Word.to_nat(p, q), Word.to_nat(32n, bw)), Word.to_nat(32n, rw)) == x : Nat}, +i2: {Nat.is_lt(Word.to_nat(32n, rw), Word.to_nat(32n, bw)) == True{} : Bool}) -> {Nat.add(Nat.mul(ud.q(1n+p, U32.divmod.go.fin(p, q, U32{s}, U32{bw}, g)), U32.to_nat(U32{bw})), ud.r(1n+p, U32.divmod.go.fin(p, q, U32{s}, U32{bw}, g))) == x2 : Nat} & {Nat.is_lt(ud.r(1n+p, U32.divmod.go.fin(p, q, U32{s}, U32{bw}, g)), U32.to_nat(U32{bw})) == True{} : Bool}: match g: case True{}: ud.fin.t(p, q, bw, a0, rw, x, x2, U32.to_nat(U32.sub(U32{s}, U32{bw})), ex, i1, ud.k(32n, Word.to_nat(32n, s), Word.to_nat(32n, bw), Word.to_nat(32n, rw), U.U32Nat.bit(a0), U32.to_nat(U32.sub(U32{s}, U32{bw})), T, U32.is_lt(U32{s}, U32{bw}), True{}, eput, Equal.sym(Bool, U32.is_lt(U32{s}, U32{bw}), Nat.is_lt(Word.to_nat(32n, s), Word.to_nat(32n, bw)), Laws.u32_lt_value(U32{s}, U32{bw})), Equal.trans(Bool, Bool.or(T, Bool.not(U32.is_lt(U32{s}, U32{bw}))), Bool.or(T, U32.is_ge(U32{s}, U32{bw})), True{}, Equal.cong(Bool, Bool, zz => Bool.or(T, zz), Bool.not(U32.is_lt(U32{s}, U32{bw})), U32.is_ge(U32{s}, U32{bw}), Equal.sym(Bool, U32.is_ge(U32{s}, U32{bw}), Bool.not(U32.is_lt(U32{s}, U32{bw})), un.ge_lt(U32.cmp(U32{s}, U32{bw})))), eg), Equal.trans(Nat, Nat.add(U32.to_nat(U32.sub(U32{s}, U32{bw})), Nat.mul(1n, Word.to_nat(32n, bw))), Nat.add(Word.to_nat(32n, s), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw})))), Nat.add(Word.to_nat(32n, s), U.U32Nat.dbl(32n, Nat.mul(1n, U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw}))))), Equal.trans(Nat, Nat.add(U32.to_nat(U32.sub(U32{s}, U32{bw})), Nat.mul(1n, Word.to_nat(32n, bw))), Nat.add(U32.to_nat(U32.sub(U32{s}, U32{bw})), Word.to_nat(32n, bw)), Nat.add(Word.to_nat(32n, s), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw})))), Equal.cong(Nat, Nat, zz => Nat.add(U32.to_nat(U32.sub(U32{s}, U32{bw})), zz), Nat.mul(1n, Word.to_nat(32n, bw)), Word.to_nat(32n, bw), ur.r32(Word.to_nat(32n, bw))), Laws.u32_sub_wrap(U32{s}, U32{bw})), Equal.cong(Nat, Nat, zz => Nat.add(Word.to_nat(32n, s), U.U32Nat.dbl(32n, zz)), U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw})), Nat.mul(1n, U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw}))), ur.r33(U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw}))))), un.bit_le(a0), i2, Laws.word_value_lt(32n, bw))) case False{}: ud.fin.f(p, q, bw, a0, rw, x, x2, Word.to_nat(32n, s), ex, i1, ud.k(32n, Word.to_nat(32n, s), Word.to_nat(32n, bw), Word.to_nat(32n, rw), U.U32Nat.bit(a0), Word.to_nat(32n, s), T, U32.is_lt(U32{s}, U32{bw}), False{}, eput, Equal.sym(Bool, U32.is_lt(U32{s}, U32{bw}), Nat.is_lt(Word.to_nat(32n, s), Word.to_nat(32n, bw)), Laws.u32_lt_value(U32{s}, U32{bw})), Equal.trans(Bool, Bool.or(T, Bool.not(U32.is_lt(U32{s}, U32{bw}))), Bool.or(T, U32.is_ge(U32{s}, U32{bw})), False{}, Equal.cong(Bool, Bool, zz => Bool.or(T, zz), Bool.not(U32.is_lt(U32{s}, U32{bw})), U32.is_ge(U32{s}, U32{bw}), Equal.sym(Bool, U32.is_ge(U32{s}, U32{bw}), Bool.not(U32.is_lt(U32{s}, U32{bw})), un.ge_lt(U32.cmp(U32{s}, U32{bw})))), eg), ur.r34(Word.to_nat(32n, s), Word.to_nat(32n, bw), U.U32Nat.bit(U32.is_lt(U32{s}, U32{bw}))), un.bit_le(a0), i2, Laws.word_value_lt(32n, bw))) 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=Bool.or 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.double 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.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.cmp https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.divmod.go.fin https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_ge 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.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_lt_value https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_sub_wrap https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_value_lt https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ud.fin.f https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ud.fin.t https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ud.k https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ud.q https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ud.r https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.bit_le https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.ge_lt https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r32 https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r33 https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r34 https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.bit https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl