YES Confluence Proof

Confluence Proof

by Hakusan

Input

The rewrite relation of the following TRS is considered.

a(c(x)) b(a(x))
a(c(x)) a(c(x))
a(a(x)) a(b(x))
b(b(x)) a(c(x))
c(c(x)) c(a(x))
c(b(x)) a(c(x))
a(b(x)) a(c(x))
a(c(x)) a(c(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:
a(c(x)) b(a(x))
a(a(x)) a(b(x))
c(c(x)) c(a(x))
c(b(x)) a(c(x))
a(b(x)) a(c(x))
Consequently, PCPS(R,C) is included in the following TRS P where steps are used to show that certain pairs are C-convertible.

There are no rules.


Relative termination of P / R is proven as follows.

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 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:
a(c(x)) b(a(x))
a(a(x)) a(b(x))
c(c(x)) c(a(x))
a(b(x)) a(c(x))
Consequently, PCPS(R,C) is included in the following TRS P where steps are used to show that certain pairs are C-convertible.

There are no rules.


Relative termination of P / R is proven as follows.

1.2.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.2 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.
a(c(c(x1_1))) a(c(a(x1_1)))
a(c(c(x1_1))) b(a(c(x1_1)))
a(a(c(x1_1))) a(b(a(x1_1)))
a(a(c(x1_1))) a(b(c(x1_1)))
a(a(a(x1_1))) a(a(b(x1_1)))
a(a(a(x1_1))) a(b(a(x1_1)))
a(a(b(x1_1))) a(a(c(x1_1)))
a(a(b(x1_1))) a(b(b(x1_1)))
c(c(c(x1_1))) c(c(a(x1_1)))
c(c(c(x1_1))) c(a(c(x1_1)))

Relative termination of P / R is proven as follows.

1.2.2.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[a(x1)] =
1 1 1
0 1 1
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[c(x1)] =
1 0 1
0 0 0
0 1 1
· x1 +
0 0 0
0 0 0
1 0 0
[b(x1)] =
1 0 1
0 1 1
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
the rules
a(a(c(x1_1))) a(b(c(x1_1)))
a(a(a(x1_1))) a(a(b(x1_1)))
a(a(b(x1_1))) a(a(c(x1_1)))
remain in R. Moreover, the rules
a(a(x)) a(b(x))
a(b(x)) a(c(x))
remain in S.

1.2.2.1.1 Rule Removal

Using the recursive path order with the following precedence and status
prec(b) = 2 stat(b) = lex
prec(a) = 2 stat(a) = lex
prec(c) = 0 stat(c) = lex
the rules
a(a(c(x1_1))) a(b(c(x1_1)))
a(a(a(x1_1))) a(a(b(x1_1)))
remain in R. Moreover, the rule
a(a(x)) a(b(x))
remains in S.

1.2.2.1.1.1 Rule Removal

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

1.2.2.1.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.2.2 (Weakly) Orthogonal

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

Tool configuration

Hakusan