def up_x

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

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/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

38# x < (high(t, x) + 1) 2^t
39def up_x(+t: Nat, +x: Nat) -> {Nat.is_lt(x, C.shift(t, 1n+C.high(t, x))) == True{} : Bool}:
40  +h = C.high(t, x)
41  +l0 = C.low(t, x)
42  +s = C.shift(t, h)
43  +p = C.pow2(t)
44  +a1 = Equal.trans(Bool, Nat.is_lt(Nat.add(l0, s), Nat.add(p, s)), Nat.is_lt(l0, p), True{}, WW.lt_cancel_r(l0, p, s), WW.low_lt(t, x))
45  +e1 = Equal.trans(Nat, Nat.add(p, s), Nat.add(C.shift(t, 1n), s), C.shift(t, 1n+h), Equal.cong(Nat, Nat, z => Nat.add(z, s), p, C.shift(t, 1n), Equal.sym(Nat, C.shift(t, 1n), p, WW.shift_one(t))), Equal.sym(Nat, C.shift(t, Nat.add(1n, h)), Nat.add(C.shift(t, 1n), s), WW.shift_add(t, 1n, h)))
46  +a2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(l0, s), z) == True{} : Bool}, Nat.add(p, s), C.shift(t, 1n+h), e1, a1)
47  L.subst(Nat, z => {Nat.is_lt(z, C.shift(t, 1n+h)) == True{} : Bool}, Nat.add(l0, s), x, Equal.sym(Nat, x, Nat.add(l0, s), WW.low_high(t, x)), a2)