YES
Confluence Proof
Confluence Proof
by csi
Input
The rewrite relation of the following TRS is considered.
|
f(g(x)) |
→ |
h(g(x),g(x)) |
|
f(s(x)) |
→ |
h(s(x),s(x)) |
|
g(x) |
→ |
s(x) |
Proof
1 Decreasing Diagrams
1.1 Relative Termination Proof
The duplicating rules (R) terminate relative to the other rules (S).
1.1.1 Rule Removal
Using the
recursive path order with the following precedence and status
| prec(s) |
= |
0 |
|
stat(s) |
= |
lex
|
| prec(h) |
= |
0 |
|
stat(h) |
= |
lex
|
| prec(f) |
= |
1 |
|
stat(f) |
= |
lex
|
| prec(g) |
= |
1 |
|
stat(g) |
= |
lex
|
all rules of R could be removed.
Moreover,
all rules of S could be removed.
1.1.1.1 R is empty
There are no rules in the TRS R. Hence, R/S is relative terminating.
1.2 Rule Labeling
Confluence is proven, because all critical peaks can be joined decreasingly
using the following rule labeling function (rules that are not shown have label 0).
-
f(g(x))→h(g(x),g(x)) ↦ 3
-
f(s(x))→h(s(x),s(x)) ↦ 0
-
g(x)→s(x) ↦ 0
All critical pairs are joinable:
-
f(s(x))→h(s(x),s(x))←h(g(x),s(x))←h(g(x),g(x))
-
f(s(x))→h(s(x),s(x))←h(s(x),g(x))←h(g(x),g(x))
Tool configuration
csi
- version: csi 1.2.5 [hg: unknown]
- strategy:
(if left-linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)!