 A first-order language with \(\mid^-\) as the only operator is assumed. (\(F\) and \(G\) are metavariables for predicates in the predicate functor language.) \(\wr^n\) \(\textit{Inv}^n\), \(\textit{inv}^n\), \(\textit{Pad}^{n+1}\)  and \(\textit{Ref}^n\) are predicate functors, for every  \(n\in\omega\). A formula of FOL is rewritten into a formula in a predicate functor language by applications of the following clauses.