~/jendhub

def uq.inc_wz

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

import bend-osdev-algo@0.1.0.0/proof_u32.bend as ProofU32
import Base

510def uq.inc_wz(+n: Nat, +w: Word(n), +z: Word(n), h: {Nat.is_le(1n+Word.to_nat(n, w), Word.to_nat(n, z)) == True{} : Bool}) -> {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}:
511  uq.inc_w(n, w, uq.le_lt_trans(1n+Word.to_nat(n, w), Word.to_nat(n, z), uq.pw(n), h, uq.val_lt(n, z)))

Uses (10)

Used by (1)