~/jendhub

def uq.u32_inc

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

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

513# 1 + a <= c: U32.inc(a) is 1 + a
514def uq.u32_inc(a: U32, c: U32, h: {Nat.is_le(1n+U32.to_nat(a), U32.to_nat(c)) == True{} : Bool}) -> {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}:
515  match a c:
516    case U32{+w} U32{+z}:
517      uq.inc_wz(32n, w, z, h)

Uses (7)

Used by (1)