~/jendhub

def tb.e8

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

import bend-osdev-acpi@0.1.1.0/PROOF_tables.bend as PROOFTables
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

323def tb.e8(+v: W.W64) -> {Nat.add(B.Octets.len(B.Octets.le64(v)), 0n) == 8n : Nat}:
324  %Equal.sym(Nat, B.Octets.len(B.Octets.le64(v)), 8n, BL.octets_len_le64(v)) : {Nat.add(_, 0n) == 8n : Nat}
325  {==}

Uses (7)

Used by (1)