The Question: Why Append to the Back?

AC-3 maintains a queue of arcs. When REMOVE-INCONSISTENT-VALUES prunes DOMAIN[Xᵢ], every arc (Xₖ, Xᵢ) pointing at Xᵢ gets re-enqueued — at the back. A natural objection: the arcs we just invalidated are the freshest leads. Shouldn't they jump the queue and get processed immediately, instead of waiting behind everything already in line?

The answer splits cleanly into two layers:

Correctness: the order is completely irrelevant — any fair schedule reaches the same final domains.
Efficiency: back-of-queue (FIFO) is often the better default, for a batching reason that is easy to miss.

Layer 1: Correctness — A Fixpoint Doesn't Care How You Approach It

The lattice setup

Collect all domain vectors into one space:

$L = \mathcal{P}(D_1) \times \cdots \times \mathcal{P}(D_n)$

ordered componentwise by inclusion ⊑. Since every Dᵢ is finite, L is a finite complete lattice. Each arc (i, j) defines a revise operator Rᵢⱼ : L → L that touches only component i:

$R_{ij}(D)_i = \{\, x \in D_i : \exists\, y \in D_j,\ (x,y) \text{ satisfies the constraint} \,\}$

Three properties do all the work:

Property	Statement	Why it holds
Reductive	Rᵢⱼ(D) ⊑ D	Revise only deletes values, never adds
Monotone	D ⊑ D′ ⟹ Rᵢⱼ(D) ⊑ Rᵢⱼ(D′)	If x finds a support y in the smaller Dⱼ′, it certainly finds one in the larger Dⱼ. Smaller domains ⟹ fewer survivors. This is the load-bearing property.
Finite descent	No infinite strictly decreasing chain in L	L is finite; every strict step deletes ≥ 1 value

The chaotic iteration theorem

Theorem (Cousot & Cousot, chaotic iteration). Apply the operators {Rᵢⱼ} in any fair order — fair meaning every arc invalidated by a domain change is eventually re-examined, which is exactly what AC-3's queue mechanism enforces. Then the iteration terminates in finitely many steps, and every fair schedule stops at the same point: the greatest fixpoint gfp = the largest arc-consistent sub-domain contained in the initial domains.

Proof sketch (a lattice squeeze argument):

Termination: reductive + finite descent ⟹ any fair sequence stabilizes at some common fixpoint D*.
Lower bound: let M be any arc-consistent domain vector with M ⊑ D⁽⁰⁾. Induct on steps: if M ⊑ D⁽ᵗ⁾, then by monotonicity M = Rᵢⱼ(M) ⊑ Rᵢⱼ(D⁽ᵗ⁾) = D⁽ᵗ⁺¹⁾. So M stays below the iterate at every step of every schedule — no order can ever "accidentally" delete a value that belongs to the answer.