def uq.add_wz

bend-osdev-algo@0.1.0.0 · proof_u32.bend:486

import Base

486# the bound given by a word's value, so that 2^n is never expanded
487def uq.add_wz(+n: Nat, +a: Word(n), +b: Word(n), +c: Bool, +z: Word(n), h: {Nat.is_le(Nat.add(uq.cv(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))), Word.to_nat(n, z)) == True{} : Bool}) -> {Word.to_nat(n, Word.adc(n, a, b, False{}, c)) == Nat.add(uq.cv(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}:
488  uq.add_w(n, a, b, c, uq.le_lt_trans(Nat.add(uq.cv(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))), Word.to_nat(n, z), uq.pw(n), h, uq.val_lt(n, z)))