Hmm... I have an idea. I've spent the whole weekend working on my thesis, so I might as well share a little bit of it.

"Remember that a CLp-term is a legal pattern if it is linear, it is either a non-application or an application which does not unify with the left-hand side of a Wp rule, and all its proper subterms are patterns.

The first of these requirements is met due to the fact that, by convention, the names of the variables in all patterns (in this case P_1, P_2, Q_1 and Q_2) are different. P_1 »« Q_1 may only contain variables present in P_1 or Q_1 (which are not present in P_2 nor Q_2), while P_2 »« Q_2 may only contain variables present in P_2 or Q_2 (which are not present in P_1 nor Q_1). This means that P_1 »« Q_1 and P_2 »« Q_2 have no variables in common. We also know by induction hypothesis that P_1 »« Q_1 and P_2 »« Q_2 are patterns (and are therefore linear). Hence, (P_1P_2) »« (Q_1Q_2), defined as (P_1 »« Q_1)(P_2 »« Q_2), is also linear.

The second requirement is also met: P_1P_2 is a pattern, and thus it does not unify with the left-hand side of any Wp-rule. By Corollary 17, we know that (P_1P_2)»«(Q_1Q_2) is an instance of P_1P_2. Therefore, (P_1P_2)»«(Q_1Q_2) does not unify with the left-hand side of any Wp-rule.

As for the third requirement, note that every proper subterm of P is a pattern, and any free variables in P can only be substituted in P»«Q by subterms of Q, which are also patterns. The only remaining possibility for P»«Q not to be a pattern would be if a proper prefix of P»«Q unified with the left-hand side of a Wp rule, but this is impossible because, since P is a pattern, all of its applicative prefixes must meet the second requirement, and if two terms do not unify, no instance of either of them can unify with the other."

What's the connection to the subject? Well... I missed it.