def hpos_le_w

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64est.bend:150

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/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

150# 1 <= high(t, b) for t <= 32 and b >= 2^32
151# the bound 2^w stays open (w is 32 at the use): a closed 2^32 is expanded
152def hpos_le_w(+w: Nat, +lo: Nat, +h: Nat, +t: Nat, +tw: {Nat.is_le(t, w) == True{} : Bool}, +hh: {Nat.is_eq(h, 0n) == False{} : Bool}) -> {Nat.is_le(1n, C.high(t, Nat.add(lo, C.shift(w, h)))) == True{} : Bool}:
153  +bv = Nat.add(lo, C.shift(w, h))
154  +a1 = WW.shift_mono(w, 1n, h, WA.pos_ne(h, hh))
155  +a2 = L.subst(Nat, z => {Nat.is_le(C.shift(w, h), z) == True{} : Bool}, Nat.add(C.shift(w, h), lo), bv, N.add_comm(C.shift(w, h), lo), N.le_add_right(C.shift(w, h), lo))
156  +a3 = L.subst(Nat, z => {Nat.is_le(z, bv) == True{} : Bool}, C.shift(w, 1n), C.pow2(w), WW.shift_one(w), N.le_trans(C.shift(w, 1n), C.shift(w, h), bv, a1, a2))
157  +hle = N.le_trans(C.pow2(t), C.pow2(w), bv, N.pow2_mono(t, w, tw), a3)
158  WA.pos_ne(C.high(t, bv), hpos(t, bv, Nat.is_eq(C.high(t, bv), 0n), {==}, hle))