YES Confluence Proof

Confluence Proof

by Hakusan

Input

The rewrite relation of the following TRS is considered.

f(f(x)) → f(g(f(x)))

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(x1_1))) → f(f(g(f(x1_1))))
f(f(f(x1_1))) → f(g(f(f(x1_1))))

Relative termination of P / R is proven as follows.

1.1 Rule Removal

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the naturals
[g(x1)] =
1 0
0 0
· x1 +
0 0
0 0
[f(x1)] =
1 2
0 0
· x1 +
1 0
1 0
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