def tb.dm8

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

import Base

279def tb.dm8(+n: Nat, +d: Nat) -> {Nat.divmod.go(Nat.mul(n, 8n), 7n, d, 0n) == (Nat.add(n, d), 0n) : Nat & Nat}:
280  match n:
281    case 0n:
282      {==}
283    case 1n+p:
284      %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}
285      %tb.asr(p, d) : {(_, 0n) == (Nat.add(1n+p, d), 0n) : Nat & Nat}
286      {==}