Order formation

This quotient collapses cyclic components; it does not prove that cycles are precisely inconsistent records. For example, the Boolean constraints $a=b,b=a$ are consistent, whereas $a=1-b,b=a$ are not. Strong normalization concerns legal reduction sequences and cannot substitute for an analysis of such constraint systems.