def li.mask_mask

bend-osdev-mode-core@0.1.0.0 · PROOF.bend:113

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

113def li.mask_mask(zs: List<&2, U32>) -> {B.mask(B.mask(zs)) == B.mask(zs) : List<&2, U32>}:
114  match zs:
115    case Nil{}:
116      {==}
117    case Con{+z, +t}:
118      %bits.byte_byte(z) : {Con{B.byte(B.byte(z)), B.mask(B.mask(t))} == Con{_, B.mask(t)} : List<&2, U32>}
119      %li.mask_mask(t) : {Con{B.byte(B.byte(z)), B.mask(B.mask(t))} == Con{B.byte(B.byte(z)), _} : List<&2, U32>}
120      {==}