YES Confluence Proof

Confluence Proof

by Hakusan

Input

The rewrite relation of the following TRS is considered.

f(f(f(x))) a
f(f(a)) a
f(a) a
f(f(g(g(x)))) f(a)
g(f(a)) a
g(a) a

Proof

1 Compositional Parallel Critical Pair Systems

All parallel critical pairs of the TRS R are joinable by R. This can be seen as follows: The parallel critical pairs can be joined as follows. Here, ↔ is always chosen as an appropriate rewrite relation which is automatically inferred by the certifier.
The TRS C is chosen as:

There are no rules.

Consequently, PCPS(R,C) is included in the following TRS P where steps are used to show that certain pairs are C-convertible.
f(f(f(f(x1_1)))) f(a)
f(f(f(f(x1_1)))) a
f(f(f(a))) f(a)
f(f(f(a))) a
f(f(f(g(g(x1_1))))) f(f(a))
f(f(f(g(g(x1_1))))) a
f(f(f(f(f(x2_1))))) f(f(a))
f(f(f(f(f(x2_1))))) a
f(f(f(f(a)))) f(f(a))
f(f(f(f(a)))) a
f(f(f(a))) f(f(a))
f(f(f(f(g(g(x2_1)))))) f(f(f(a)))
f(f(f(f(g(g(x2_1)))))) a
f(f(a)) f(a)
f(f(a)) a
f(f(g(g(f(a))))) f(f(g(a)))
f(f(g(g(f(a))))) f(a)
f(f(g(g(a)))) f(f(g(a)))
f(f(g(g(a)))) f(a)
g(f(a)) g(a)
g(f(a)) a

Relative termination of P / R is proven as follows.

1.1 Rule Removal

Using the recursive path order with the following precedence and status
prec(g) = 2 stat(g) = lex
prec(a) = 0 stat(a) = lex
prec(f) = 0 stat(f) = lex
all rules of R could be removed. Moreover, all rules of S could be removed.

1.1.1 R is empty

There are no rules in the TRS R. Hence, R/S is relative terminating.


Confluence of C is proven as follows.

1.2 (Weakly) Orthogonal

Confluence is proven since the TRS is (weakly) orthogonal.

Tool configuration

Hakusan