This paper studies completion in the case of 
equations with constraints consisting of 
first-order formulae over equations, disequations, 
and an irreducibility predicate. We present several 
inference systems which show in a very precise way 
how to take advantage of redundancy notions in this 
framework.  A notable feature of these systems is the
variety of tradeoffs they present for removing redundant 
instances of the equations involved in an inference. 
The irreducibility predicates simulate redundancy 
criteria based on reducibility (such as prime 
superposition and Blocking in Basic Completion)
and the disequality predicates simulate the notion of 
subsumed critical pairs; in addition, since constraints 
are passed along with equations, we can perform hereditary 
versions of all these redundancy checks.  This combines
in one consistent framework stronger versions of all 
practical critical pair criteria.  We also provide a 
rigorous analysis of the problem with completing sets of 
equations with initial constraints.  Finally, an interesting 
consequence concerning the recalculation of critical pairs 
in completion procedures is discussed.