~/jendhub

def ckp.l1r

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

import bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend as PROOFChecksum
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

94def ckp.l1r(+a: Nat, +b: Nat) -> {U.U32Nat.low(8n, Nat.add(a, b)) == U.U32Nat.low(8n, Nat.add(a, U.U32Nat.low(8n, b))) : Nat}:
95  %UL.nat_add_comm(b, a) : {U.U32Nat.low(8n, _) == U.U32Nat.low(8n, Nat.add(a, U.U32Nat.low(8n, b))) : Nat}
96  %UL.nat_add_comm(U.U32Nat.low(8n, b), a) : {U.U32Nat.low(8n, Nat.add(b, a)) == U.U32Nat.low(8n, _) : Nat}
97  ckp.l1(b, a)

Uses (5)

Used by (1)