def wd.bt

bend-osdev-word64@0.1.1.0 · PROOF_div.bend:98

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

98def wd.bt(x: Nat, h: {Nat.is_lt(x, U.U32Nat.dbl(1n, 1n)) == True{} : Bool}) -> {U.U32Nat.bit(Nat.is_eq(x, 1n)) == x : Nat}:
99  match x:
100    case 0n:
101      {==}
102    case 1n+ +p:
103      match p:
104        case 0n:
105          {==}
106        case 1n+ +q:
107          match q:
108            case 0n:
109              Empty.absurd({U.U32Nat.bit(Nat.is_eq(2n, 1n)) == 2n : Nat}, wn.ft(h))
110            case 1n+ +r:
111              Empty.absurd({U.U32Nat.bit(Nat.is_eq(3n+r, 1n)) == 3n+r : Nat}, wn.ft(h))