Vergleiche

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

• (x₀ > y₀)∧(tail(x) = tail(y))
• oder tail(x) > tail(y)

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

• | x| = | y| = 0
• oder (x₀ = y₀)∧(tail(x) = tail(y))

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