The CAD Conundrum: Lex-Least vs Order

This paper is part of our ongoing research and collaboration on understanding the relations between CAD algorithms, equational constraints and curtains. Our previous work manages to circumvent the curtain problem in the single equational constraint by taking advantage of the Lex-least valuation (even in the presence of curtains). That method however fails to take full advantage of multiple equational constraints. In this paper we provide further clarification of McCallum's work to validate the use of restricted projection operator at 2 levels. We also discuss the close relationship between order invariant and lex-least invariant CAD's.