def hi16_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mul.bend:83

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/u32div.bend as UD
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR

83def hi16_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +c: U32, +pc: {c == U32{WD.pw(32n, 16n)} : U32}) -> {Nat.is_lt(hi16(x, c), WD.sc(16n, one)) == True{} : Bool}:
84  +le = L.subst(Nat, z => {Nat.is_le(WD.sc(16n, hi16(x, c)), z) == True{} : Bool}, Nat.add(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))), v(x), dm16(one, h1, x, c, pc), N.le_add_right(WD.sc(16n, hi16(x, c)), v(U32.mod(x, c))))
85  +lt = N.le_lt_trans(WD.sc(16n, hi16(x, c)), v(x), WD.sc(32n, one), le, UD.vb(one, h1, x))
86  AR.sc_lt_cancel(16n, hi16(x, c), WD.sc(16n, one), L.subst(Nat, z => {Nat.is_lt(WD.sc(16n, hi16(x, c)), z) == True{} : Bool}, WD.sc(32n, one), WD.sc(16n, WD.sc(16n, one)), AR.sc_idx(16n, 16n, one), lt))