PROOFTables.tb.gas_a: def of bend-osdev-acpi@0.1.1.0
Import: import bend-osdev-acpi@0.1.1.0/PROOF_tables.bend as PROOFTables
Lines 42-43 of bend-osdev-acpi@0.1.1.0/PROOF_tables.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.1.0/PROOF_tables.bend&start_line=42&end_line=43

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL

def tb.gas_a(+a: B.Octets, +s: U32, +w: U32, +off: U32, +acc: U32, +addr: W.W64, +b: B.Octets) -> {Some{addr} == B.Octets.le64_at(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n)) : Maybe<&2, W.W64>}:
  Equal.sym(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n)), Some{addr}, Equal.trans(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b))), Nat.add(B.Octets.len(a), 4n)), B.Octets.le64_at(B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b)), 4n), Some{addr}, BL.octets_le64_at_append_add(a, B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b)), 4n), Equal.trans(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b)), 4n), B.Octets.le64_at(B.Octets.append(B.Octets.le64(addr), b), 0n), Some{addr}, BL.octets_le64_at_append_add(B.Octets.of_list([s, w, off, acc]), B.Octets.append(B.Octets.le64(addr), b), 0n), Equal.trans(Maybe<&2, W.W64>, B.Octets.le64_at(B.Octets.append(B.Octets.le64(addr), b), 0n), B.Octets.le64_at(B.Octets.le64(addr), 0n), Some{addr}, BL.octets_le64_at_append_le(B.Octets.le64(addr), b, 0n, tb.l64(addr)), BL.octets_le64_round_trip(addr)))))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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.1.0/PROOF_tables.bend&name=tb.l64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_le64_at_append_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_le64_at_append_le
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_le64_round_trip
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.le64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.le64_at
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64