def wv.nlt

bend-osdev-word64@0.1.1.0 · proof_value.bend:315

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 UL
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

315# al < 2^n <= bl + 2^n * (1 + q)
316def wv.nlt(+n: Nat, +al: Nat, +bl: Nat, +q: Nat, hl: {Nat.is_lt(al, U.U32Nat.dbl(n, 1n)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 1n+q))) == True{} : Bool}:
317  +k = U.U32Nat.dbl(n, 1n)
318  +e0 = Equal.trans(Nat, al, Nat.add(al, 0n), Nat.add(al, U.U32Nat.dbl(n, 0n)), Equal.sym(Nat, Nat.add(al, 0n), al, UL.nat_add_zero(al)), Equal.cong(Nat, Nat, v => Nat.add(al, v), 0n, U.U32Nat.dbl(n, 0n), Equal.sym(Nat, U.U32Nat.dbl(n, 0n), 0n, UL.dbl_zero(n))))
319  +s1 = Equal.trans(Bool, Nat.is_le(k, U.U32Nat.dbl(n, 1n+q)), Nat.is_le(1n, 1n+q), True{}, UL.dbl_le(n, 1n, 1n+q), wn.le_zero(q))
320  +s2 = UO.nat_lt_le_trans(al, k, U.U32Nat.dbl(n, 1n+q), hl, s1)
321  +s3 = UO.nat_lt_le_trans(al, U.U32Nat.dbl(n, 1n+q), Nat.add(bl, U.U32Nat.dbl(n, 1n+q)), s2, UL.nat_le_add(U.U32Nat.dbl(n, 1n+q), bl))
322  wn.lt_rw(al, Nat.add(al, U.U32Nat.dbl(n, 0n)), Nat.add(bl, U.U32Nat.dbl(n, 1n+q)), e0, s3)