def vb_pos

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64dmrem.bend:26

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/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/w64add.bend as WA
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/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dm.bend as DM

26def vb_pos(+bl: U32, +bh: U32, +hz: {U32.is_zero(bh) == False{} : Bool}) -> {Nat.is_le(1n, SW.value(WU.U64{bl, bh})) == True{} : Bool}:
27  +h1 = WA.pos_ne(DM.v(bh), Equal.trans(Bool, Nat.is_eq(DM.v(bh), 0n), U32.is_zero(bh), False{}, Equal.sym(Bool, U32.is_zero(bh), Nat.is_eq(DM.v(bh), 0n), LW.zero_nat(bh)), hz))
28  N.le_trans(1n, DM.v(bh), SW.value(WU.U64{bl, bh}), h1, N.le_trans(DM.v(bh), C.shift(32n, DM.v(bh)), SW.value(WU.U64{bl, bh}), WW.shift_ge(32n, DM.v(bh)), L.subst(Nat, z => {Nat.is_le(C.shift(32n, DM.v(bh)), z) == True{} : Bool}, Nat.add(C.shift(32n, DM.v(bh)), DM.v(bl)), SW.value(WU.U64{bl, bh}), N.add_comm(C.shift(32n, DM.v(bh)), DM.v(bl)), N.le_add_right(C.shift(32n, DM.v(bh)), DM.v(bl)))))