Formal inverse on actual tests

The inner expression

is an actual smooth compact test. It is formed before the next Green operation. In terms of the inherited rule, (eq:iteration) can be written as applying that rule to $F_{-a_c}$, not to an unspecified representative of $\mathbf{\varphi }(-a_c)$.