PROOFChecksum.ckp.nsapp: def of bend-osdev-acpi@0.1.2.0
Import: import bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend as PROOFChecksum
Lines 166-172 of bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend&start_line=166&end_line=172

import Base
import bend-osdev-bytes@0.1.1.1/bytes.bend as B
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

def ckp.nsapp(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {ckp.ns(B.append(xs, ys)) == Nat.add(ckp.ns(xs), ckp.ns(ys)) : Nat}:
  match xs:
    case Nil{}:
      {==}
    case Con{+h, +t}:
      %Equal.sym(Nat, ckp.ns(B.append(t, ys)), Nat.add(ckp.ns(t), ckp.ns(ys)), ckp.nsapp(t, ys)) : {Nat.add(U32.to_nat(U32.and(255, h)), _) == Nat.add(ckp.ns(Con{h, t}), ckp.ns(ys)) : Nat}
      Equal.sym(Nat, Nat.add(Nat.add(U32.to_nat(U32.and(255, h)), ckp.ns(t)), ckp.ns(ys)), Nat.add(U32.to_nat(U32.and(255, h)), Nat.add(ckp.ns(t), ckp.ns(ys))), UL.nat_add_assoc(U32.to_nat(U32.and(255, h)), ckp.ns(t), ckp.ns(ys)))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_checksum.bend&name=ckp.ns
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_assoc