def wv.g

bend-osdev-word64@0.1.1.0 · PROOF_div.bend:30

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-word64@0.1.1.0/proof_value.bend as P

30def wv.g(+n: Nat, +m: Nat, +h: Word(n), +l: Word(n), e: {Nat.add(n, n) == m : Nat}) -> {Nat.is_lt(P.wv.V(n, h, l), U.U32Nat.dbl(m, 1n)) == True{} : Bool}:
31  %e : {Nat.is_lt(P.wv.V(n, h, l), U.U32Nat.dbl(_, 1n)) == True{} : Bool}
32  %UL.dbl_dbl(n, n, 1n) : {Nat.is_lt(P.wv.V(n, h, l), _) == True{} : Bool}
33  P.wv.val_lt2(n, Word.to_nat(n, l), Word.to_nat(n, h), UL.word_value_lt(n, l), UL.word_value_lt(n, h))