PROOFTables.tb.xlen: def of bend-osdev-acpi@0.1.2.0
Import: import bend-osdev-acpi@0.1.2.0/PROOF_tables.bend as PROOFTables
Lines 297-306 of bend-osdev-acpi@0.1.2.0/PROOF_tables.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_tables.bend&start_line=297&end_line=306

import Base
import bend-osdev-word64@0.1.1.1/word64.bend as W
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/rsdt.bend as R

def tb.xlen(+xs: List<&2, W.W64>) -> {Nat.mul(List.length(&2, W.W64, xs), 8n) == B.Octets.len(B.Octets.concat(R.sl.enc(xs, True{}))) : Nat}:
  match xs:
    case Nil{}:
      {==}
    case Con{x, t}:
      %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.le64(x), R.sl.enc(t, True{})}), B.Octets.append(B.Octets.le64(x), B.Octets.concat(R.sl.enc(t, True{}))), BL.octets_concat_cons(B.Octets.le64(x), R.sl.enc(t, True{}))) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 8n) == B.Octets.len(_) : Nat}
      %tb.la(B.Octets.le64(x), B.Octets.concat(R.sl.enc(t, True{}))) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 8n) == _ : Nat}
      %Equal.sym(Nat, B.Octets.len(B.Octets.le64(x)), 8n, BL.octets_len_le64(x)) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 8n) == Nat.add(_, B.Octets.len(B.Octets.concat(R.sl.enc(t, True{})))) : Nat}
      %tb.xlen(t) : {Nat.mul(List.length(&2, W.W64, Con{x, t}), 8n) == Nat.add(8n, _) : Nat}
      {==}

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=List.length
  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=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_tables.bend&name=tb.la
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/rsdt.bend&name=sl.enc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/LAWS.bend&name=octets_concat_cons
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/LAWS.bend&name=octets_len_le64
  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.concat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.le64
  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-word64@0.1.1.1/word64.bend&name=W64