Certification Problem
Input (COPS 96)
We consider the TRS containing the following rules:
|
F(H(x),y) |
→ |
F(H(x),I(I(y))) |
(1) |
|
F(x,G(y)) |
→ |
F(I(x),G(y)) |
(2) |
|
I(x) |
→ |
x |
(3) |
The underlying signature is as follows:
{F/2, H/1, I/1, G/1}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by Hakusan @ CoCo 2023)
1 Compositional Rule Labeling with Parallel Critical Pairs
Confluence is proven by compositional rule labeling with parallel critical pairs.
The following labeling functions phi and psi are used (if only one is displayed, then phi = psi).
-
|
F(H(x),y) |
→ |
F(H(x),I(I(y))) |
(1) |
↦ 2
-
|
F(x,G(y)) |
→ |
F(I(x),G(y)) |
(2) |
↦ 3
-
↦ 1
-
|
F(H(x),y) |
→ |
F(H(x),I(I(y))) |
(1) |
↦ 2
-
|
F(x,G(y)) |
→ |
F(I(x),G(y)) |
(2) |
↦ 3
-
↦ 1
The non-0-0 parallel critical pairs are joined as follows.
The remaining rules are handled recursively.
There are no rules.
1.1 (Weakly) Orthogonal
Confluence is proven since the TRS is (weakly) orthogonal.