~/jendhub

def bitw.ctz_clz.h

bend-osdev-algo@0.1.0.0 · PROOF.bend:512

import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF
import Base

512def bitw.ctz_clz.h(+k: Nat, +m: Nat, l: Nat, e: {Nat.is_le(1n+k, l) == True{} : Bool}, f: {Nat.is_le(l, 1n+m) == True{} : Bool}) -> {Nat.is_le(Nat.add(k, Nat.sub(1n+m, l)), m) == True{} : Bool}:
513  match l:
514    case 0n:
515      Empty.absurd({Nat.is_le(Nat.add(k, 1n+m), m) == True{} : Bool}, absurd.ft(e))
516    case 1n+i:
517      nat.add_sub_le(k, i, m, e, f)

Uses (8)

Used by (1)