PROOFTables.tb.dm8: def of bend-osdev-acpi@0.1.1.0
Import: import bend-osdev-acpi@0.1.1.0/PROOF_tables.bend as PROOFTables
Lines 279-286 of bend-osdev-acpi@0.1.1.0/PROOF_tables.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&start_line=279&end_line=286

import Base

def tb.dm8(+n: Nat, +d: Nat) -> {Nat.divmod.go(Nat.mul(n, 8n), 7n, d, 0n) == (Nat.add(n, d), 0n) : Nat & Nat}:
  match n:
    case 0n:
      {==}
    case 1n+p:
      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.mul(p, 8n), 7n, 1n+d, 0n), (Nat.add(p, 1n+d), 0n), tb.dm8(p, 1n+d)) : {_ == (Nat.add(1n+p, d), 0n) : Nat & Nat}
      %tb.asr(p, d) : {(_, 0n) == (Nat.add(1n+p, d), 0n) : Nat & Nat}
      {==}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.divmod.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&name=tb.asr