def tb.e4

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

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

327def tb.e4(+v: U32) -> {Nat.add(B.Octets.len(B.Octets.le32(v)), 0n) == 4n : Nat}:
328  %Equal.sym(Nat, B.Octets.len(B.Octets.le32(v)), 4n, BL.octets_len_le32(v)) : {Nat.add(_, 0n) == 4n : Nat}
329  {==}