def tb.dm4

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

import Base

270def tb.dm4(+n: Nat, +d: Nat) -> {Nat.divmod.go(Nat.mul(n, 4n), 3n, d, 0n) == (Nat.add(n, d), 0n) : Nat & Nat}:
271  match n:
272    case 0n:
273      {==}
274    case 1n+p:
275      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.mul(p, 4n), 3n, 1n+d, 0n), (Nat.add(p, 1n+d), 0n), tb.dm4(p, 1n+d)) : {_ == (Nat.add(1n+p, d), 0n) : Nat & Nat}
276      %tb.asr(p, d) : {(_, 0n) == (Nat.add(1n+p, d), 0n) : Nat & Nat}
277      {==}