<critical-pairs-command> ::= critical-pairs <names> with <names>
critical-pairs *Hyp with *
LP also computes critical pairs in response to the complete command. LP keeps track of which rewrite rules have had their critical pairs computed, and does not recompute critical pairs between those rules. See also the forget command.
Critical pair equations between two rewrite rules result from using them to rewrite a common term in two different ways. Suppose that R1 is the rewrite rule l1 -> r1 and R2 is l2 -> r2. Suppose also that R1 and R2 have no variables in common (LP ensures that this is the case by substituting fresh variables for those in R2). If l2 can be unified with a nonvariable subterm of l1, then both R1 and R2 can be used to rewrite some substitution instance of l1. A critical pair equation between R1 and R2 is an equation relating the results of these two rewritings.
More precisely, if s1 is a nonvariable subterm of l1 that does not contain any variables bound by outer quantifiers in l1, if sigma is a substitution that unifies l2 with s1 and that does not introduce any variables bound by outer quantifiers in l1, and if l1' is the result of substituting r2 for s2 in l1, then sigma(l1') = sigma(r1) is a critical pair equation between R1 and R2.
Examples:
When the principal operator of l1 or l2 is an ac operator, say *, LP generalizes the critical pair computation by computing Petersen-Stickel extensions Ri' having the form li*x -> ri*x of R1 and R2, and then by computing critical pair equations between {R1, R1'} and {R2, R2'}. Thus, i(x) * x -> e has three nontrivial critical pair equations with itself when * is ac:Rewrite rules Critical pair equations 1. f(x) * f(y) -> f(x * y) b * f(y) = f(a * y) f(a) -> b f(x) * b = f(x * a) 2. P(x) => Q(x) -> true true => Q(c) <=> true P(c) -> true ... which reduces to Q(c) 3. \E x (f(x) = g(y)) -> true \E x (f(x) = c) g(c) -> c