- `trunc (binop (Y, (ext X))) --> binop ((trunc Y), X)`
- `trunc (binop (ext X), Y) --> binop X, (trunc Y)`
- `trunc (binop (X, C)) --> binop (trunc (X), C')`
- `trunc (binop C, X) --> binop (trunc C', X)`
- `zext(trunc(X) & C) -> (X & zext(C))`
- `zext (and (trunc X), C) --> and X, (zext C)`
