def F_len

bend-osdev-bytes@0.1.1.0 · PROOF.bend:310

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

310def F_len(+ws: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, ws) == B.w8s.len.fast(ws) : Nat}:
311  Equal.sym(Nat, B.w8s.len.fast(ws), List.length(&2, B.OctByte, ws),
312    Equal.trans(Nat, B.w8s.len.go(ws, 0n), Nat.add(List.length(&2, B.OctByte, ws), 0n), List.length(&2, B.OctByte, ws),
313      g_len(ws, 0n), UL.nat_add_zero(List.length(&2, B.OctByte, ws))))