Certification Problem
Input (COPS 964)
We consider the TRS containing the following rules:
|
0(x) |
→ |
1(x) |
(1) |
|
0(0(x)) |
→ |
0(x) |
(2) |
|
3(4(5(x))) |
→ |
4(3(5(x))) |
(3) |
|
2(2(2(2(2(2(2(2(2(2(2(2(2(x))))))))))))) |
→ |
0(0(0(1(0(1(1(1(0(1(1(1(1(0(0(0(0(1(0(0(1(1(1(1(0(0(0(0(0(0(0(0(1(0(0(0(1(1(1(1(1(1(1(1(1(0(0(0(0(1(1(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) |
(4) |
|
1(1(0(0(1(1(0(1(0(0(1(0(1(1(1(1(1(0(0(1(0(1(1(1(0(1(0(0(0(0(1(0(1(1(1(1(1(0(0(1(0(0(1(1(0(0(0(0(1(1(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) |
→ |
2(2(2(2(2(2(2(2(2(2(2(2(2(x))))))))))))) |
(5) |
The underlying signature is as follows:
{0/1, 1/1, 3/1, 4/1, 5/1, 2/1}Property / Task
Prove or disprove confluence.Answer / Result
No.Proof (by csi @ CoCo 2023)
1 Persistent Decomposition (Many-Sorted)
Non-confluence
is proven, because
a
system
induced by the sorts in the following many-sorted sort attachment
is not
confluent.
| 0 |
: |
2 → 2 |
| 1 |
: |
2 → 2 |
| 3 |
: |
0 → 0 |
| 4 |
: |
0 → 0 |
| 5 |
: |
1 → 0 |
| 2 |
: |
2 → 2 |
The subsystem is(1.1)
|
0(x) |
→ |
1(x) |
(1) |
|
0(0(x)) |
→ |
0(x) |
(2) |
|
2(2(2(2(2(2(2(2(2(2(2(2(2(x))))))))))))) |
→ |
0(0(0(1(0(1(1(1(0(1(1(1(1(0(0(0(0(1(0(0(1(1(1(1(0(0(0(0(0(0(0(0(1(0(0(0(1(1(1(1(1(1(1(1(1(0(0(0(0(1(1(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) |
(4) |
|
1(1(0(0(1(1(0(1(0(0(1(0(1(1(1(1(1(0(0(1(0(1(1(1(0(1(0(0(0(0(1(0(1(1(1(1(1(0(0(1(0(0(1(1(0(0(0(0(1(1(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) |
→ |
2(2(2(2(2(2(2(2(2(2(2(2(2(x))))))))))))) |
(5) |
1.1 Redundant Rules Transformation
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following
modified system:
|
0(x) |
→ |
1(x) |
(1) |
|
0(0(x)) |
→ |
0(x) |
(2) |
|
2(2(2(2(2(2(2(2(2(2(2(2(2(x))))))))))))) |
→ |
0(0(0(1(0(1(1(1(0(1(1(1(1(0(0(0(0(1(0(0(1(1(1(1(0(0(0(0(0(0(0(0(1(0(0(0(1(1(1(1(1(1(1(1(1(0(0(0(0(1(1(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) |
(4) |
|
1(1(0(0(1(1(0(1(0(0(1(0(1(1(1(1(1(0(0(1(0(1(1(1(0(1(0(0(0(0(1(0(1(1(1(1(1(0(0(1(0(0(1(1(0(0(0(0(1(1(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) |
→ |
2(2(2(2(2(2(2(2(2(2(2(2(2(x))))))))))))) |
(5) |
|
0(0(x)) |
→ |
1(1(x)) |
(6) |
|
0(0(0(x))) |
→ |
1(0(x)) |
(7) |
|
0(0(x)) |
→ |
1(x) |
(8) |
|
0(0(0(x))) |
→ |
0(1(x)) |
(9) |
|
0(0(0(x))) |
→ |
0(x) |
(10) |
|
0(0(0(x790))) |
→ |
0(x790) |
(11) |
All redundant rules that were added or removed can be
simulated in 3 steps
.
1.1.1 Non-Joinable Fork
The system is not confluent due to the following forking derivations.
| t0
|
= |
0(0(x)) |
|
→
|
1(1(x)) |
|
= |
t1
|
The two resulting terms cannot be joined for the following reason:
- When applying the cap-function on both terms (where variables may be treated like constants)
then the resulting terms do not unify.