def mask_app

bend-osdev-acpi@0.1.1.0 · PROOF.bend:1991

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

1991def mask_app(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.append(B.mask(a), B.mask(b)) == B.mask(B.append(a, b)) : List<&2, U32>}:
1992  match a:
1993    case Nil{}:
1994      {==}
1995    case Con{h, t}:
1996      %mask_app(t, b) : {Con{B.byte(h), B.append(B.mask(t), B.mask(b))} == Con{B.byte(h), _} : List<&2, U32>}
1997      {==}