Vergleiche

Größer: x = [x₀,...] > [y₀,...] = y, falls

• (x₀ > y₀) $\wedge$ (tail(x) = tail(y))
• oder tail(x) > tail(y)

Gleich: x = [x₀,...] = [y₀,...] = y, falls

• | x| = | y| = 0
• oder (x₀ = y₀) $\wedge$ (tail(x) = tail(y))

Damit x > y mit linear vielen Variablen und Klauseln möglich. Welches sind die besten Faktoren?