 There is an obvious similarity between \(\textit{Ref}\) and  \(\textsf{W}\), \(\textit{Pad}\) and \(\textsf{K}\), as well as \(\textit{Inv}\) and \(\textit{inv}\) and various combinators with permutative effects (e.g., \(\textsf{C}\) and \(\textsf{T}\)). If \(\mid^-\) is the only operator in the first-order language, then all formulas, which are not atomic, are almost of the form of the left-hand side expression in 2. What has to be assured is that the side condition is satisfied, and that is where clauses 3–6 enter. Although the various \(n\)-ary versions of \(\wr\), \(\textit{inv}\), \(\textit{Pad}\) and \(\textit{Ref}\) could be conflated (by ignoring unaffected arguments), \(\textit{Inv}\) clearly stands for infinitely many predicate functors, because \(x_1,\ldots,x_n\) cannot be ignored or omitted.