def ckp.cancel

bend-osdev-acpi@0.1.2.0 · PROOF_checksum.bend:119

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

119def ckp.cancel(+x: Nat, +a: Nat, +b: Nat, +e: {U.U32Nat.low(8n, Nat.add(x, a)) == U.U32Nat.low(8n, Nat.add(x, b)) : Nat}) -> {U.U32Nat.low(8n, a) == U.U32Nat.low(8n, b) : Nat}:
120  %UL.low_add_dbl(8n, a, U.U32Nat.high(8n, Nat.add(x, b))) : {_ == U.U32Nat.low(8n, b) : Nat}
121  %UL.low_add_dbl(8n, b, U.U32Nat.high(8n, Nat.add(x, a))) : {U.U32Nat.low(8n, Nat.add(a, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b))))) == _ : Nat}
122  %UL.nat_add_cancel(x, Nat.add(a, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b)))), Nat.add(b, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a)))), ckp.cr(x, a, b, e)) : {U.U32Nat.low(8n, Nat.add(a, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b))))) == U.U32Nat.low(8n, _) : Nat}
123  {==}