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