def p_mask_fast

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

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

572def p_mask_fast(+xs: List<&2, U32>) -> {B.mask(xs) == B.mask.fast(xs) : List<&2, U32>}:
573  Equal.sym(List<&2, U32>, B.mask.fast(xs), B.mask(xs),
574    Equal.trans(List<&2, U32>, B.mask.fast(xs), B.rev_onto(B.rev_onto(B.mask(xs), Nil{}), Nil{}), B.mask(xs),
575      Equal.cong(List<&2, U32>, List<&2, U32>, l => B.rev_onto(l, Nil{}), B.mask.go(xs, Nil{}), B.rev_onto(B.mask(xs), Nil{}), g_mask(xs, Nil{})),
576      rr_back(B.mask(xs))))