PROOFWhole.ckw.plen: def of bend-osdev-acpi@0.1.2.0
Import: import bend-osdev-acpi@0.1.2.0/PROOF_whole.bend as PROOFWhole
Lines 117-123 of bend-osdev-acpi@0.1.2.0/PROOF_whole.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_whole.bend&start_line=117&end_line=123

import Base
import bend-osdev-bytes@0.1.1.1/bytes.bend as B
import bend-osdev-bytes@0.1.1.1/LAWS.bend as BL
import bend-osdev-acpi@0.1.2.0/header.bend as H

def ckw.plen(+s: B.Octets, +l: U32, +r: U32, +sig4: {B.Octets.len(s) == 4n : Nat}) -> {B.Octets.len(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))) == 9n : Nat}:
  %Equal.sym(Nat, B.Octets.len(B.Octets.append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))), Nat.add(B.Octets.len(s), B.Octets.len(B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))), BL.octets_len_append(s, B.Octets.append(B.Octets.le32(l), H.hd.byte(r)))) : {_ == 9n : Nat}
  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.le32(l), H.hd.byte(r))), Nat.add(B.Octets.len(B.Octets.le32(l)), B.Octets.len(H.hd.byte(r))), BL.octets_len_append(B.Octets.le32(l), H.hd.byte(r))) : {Nat.add(B.Octets.len(s), _) == 9n : Nat}
  %Equal.sym(Nat, B.Octets.len(s), 4n, sig4) : {Nat.add(_, Nat.add(B.Octets.len(B.Octets.le32(l)), B.Octets.len(H.hd.byte(r)))) == 9n : Nat}
  %Equal.sym(Nat, B.Octets.len(B.Octets.le32(l)), 4n, BL.octets_len_le32(l)) : {Nat.add(4n, Nat.add(_, B.Octets.len(H.hd.byte(r)))) == 9n : Nat}
  %Equal.sym(Nat, B.Octets.len(B.Octets.of_list([r])), B.len([r]), BL.octets_len_of_list([r])) : {Nat.add(4n, Nat.add(4n, _)) == 9n : Nat}
  {==}

Uses (15):
  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=bend-osdev-acpi@0.1.2.0/header.bend&name=hd.byte
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/LAWS.bend&name=octets_len_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/LAWS.bend&name=octets_len_le32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/LAWS.bend&name=octets_len_of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.le32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=len