def tb.asr

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

import Base

250def tb.asr(+x: Nat, +a: Nat) -> {1n+Nat.add(x, a) == Nat.add(x, 1n+a) : Nat}:
251  match x:
252    case 0n:
253      {==}
254    case 1n+p:
255      %tb.asr(p, a) : {1n+1n+Nat.add(p, a) == 1n+_ : Nat}
256      {==}