def tb.dm16

bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:288

import Base

288def tb.dm16(+n: Nat, +d: Nat) -> {Nat.divmod.go(Nat.mul(n, 16n), 15n, d, 0n) == (Nat.add(n, d), 0n) : Nat & Nat}:
289  match n:
290    case 0n:
291      {==}
292    case 1n+p:
293      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.mul(p, 16n), 15n, 1n+d, 0n), (Nat.add(p, 1n+d), 0n), tb.dm16(p, 1n+d)) : {_ == (Nat.add(1n+p, d), 0n) : Nat & Nat}
294      %tb.asr(p, d) : {(_, 0n) == (Nat.add(1n+p, d), 0n) : Nat & Nat}
295      {==}