def tb.la

bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:75

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

75def tb.la(+a: B.Octets, +b: B.Octets) -> {Nat.add(B.Octets.len(a), B.Octets.len(b)) == B.Octets.len(B.Octets.append(a, b)) : Nat}:
76  Equal.sym(Nat, B.Octets.len(B.Octets.append(a, b)), Nat.add(B.Octets.len(a), B.Octets.len(b)), BL.octets_len_append(a, b))