~/jendhub

def ckw.fnh

bend-osdev-acpi@0.1.2.0 · PROOF_whole.bend:44

import bend-osdev-acpi@0.1.2.0/PROOF_whole.bend as PROOFWhole
import Base

44def ckw.fnh(+p: Nat, +z: U32, +h: {Nat.is_le(1n+p, U32.to_nat(z)) == True{} : Bool}, +ih: {U32.to_nat(U32.from_nat(p)) == p : Nat}) -> {Nat.is_le(1n+U32.to_nat(U32.from_nat(p)), U32.to_nat(z)) == True{} : Bool}:
45  %Equal.sym(Nat, U32.to_nat(U32.from_nat(p)), p, ih) : {Nat.is_le(1n+_, U32.to_nat(z)) == True{} : Bool}
46  h

Uses (7)

Used by (1)