Critical Peaks Redefined, the Non-Left_linear Case

Φ ⊔ Ψ = ⊤

In previous work we introduced clusters as terms with a number of linear patterns in them, gave both a geometric account of clusters as sets of positions and an inductive one as let-expressions for terms with gaps (second order variables), and showed these to be isomorphic giving rise to a lattice under the refinement order ⊑. This enabled us to give an alternative lattice theoretic definition of the notion of critical peak as Φ ⊔ Ψ = ⊤, for coinitial multisteps Φ and Ψ. Here we extend this to the non-linear case.