YES Confluence Proof

Confluence Proof

by Hakusan

Input

The rewrite relation of the following TRS is considered.

a(b(x))	→	a(c(x))
c(c(x))	→	c(b(x))
c(c(x))	→	c(c(x))
a(c(x))	→	c(b(x))
b(c(x))	→	a(c(x))
c(c(x))	→	c(c(x))
c(b(x))	→	a(b(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 critical peak s = a(a(c(x1_1))) _{1}←a(b(c(x1_1)))→_ε a(c(c(x1_1))) = t can be joined as follows.
s ↔ a(b(c(x1_1))) ↔ c(b(c(x1_1))) ↔ t
The critical peak s = c(c(y1)) _{ε}←c(c(y1))→_ε c(b(y1)) = t can be joined as follows.
s ↔ t
The critical peak s = c(c(b(x1_1))) _{1}←c(c(c(x1_1)))→_ε c(b(c(x1_1))) = t can be joined as follows.
s ↔ c(a(c(x1_1))) ↔ t
The critical peak s = c(c(c(x1_1))) _{1}←c(c(c(x1_1)))→_ε c(b(c(x1_1))) = t can be joined as follows.
s ↔ t
The critical peak s = c(a(b(x1_1))) _{1}←c(c(b(x1_1)))→_ε c(b(b(x1_1))) = t can be joined as follows.
s ↔ c(a(c(x1_1))) ↔ c(c(b(x1_1))) ↔ t
The critical peak s = c(b(y1)) _{ε}←c(c(y1))→_ε c(c(y1)) = t can be joined as follows.
s ↔ t
The critical peak s = c(c(b(x1_1))) _{1}←c(c(c(x1_1)))→_ε c(c(c(x1_1))) = t can be joined as follows.
s ↔ t
The critical peak s = c(c(c(x1_1))) _{1}←c(c(c(x1_1)))→_ε c(c(c(x1_1))) = t can be joined as follows.
s ↔ t
The critical peak s = c(a(b(x1_1))) _{1}←c(c(b(x1_1)))→_ε c(c(b(x1_1))) = t can be joined as follows.
s ↔ t
The critical peak s = a(c(b(x1_1))) _{1}←a(c(c(x1_1)))→_ε c(b(c(x1_1))) = t can be joined as follows.
s ↔ a(c(c(x1_1))) ↔ a(b(c(x1_1))) ↔ t
The critical peak s = a(c(c(x1_1))) _{1}←a(c(c(x1_1)))→_ε c(b(c(x1_1))) = t can be joined as follows.
s ↔ a(b(c(x1_1))) ↔ t
The critical peak s = a(a(b(x1_1))) _{1}←a(c(b(x1_1)))→_ε c(b(b(x1_1))) = t can be joined as follows.
s ↔ a(c(b(x1_1))) ↔ a(b(b(x1_1))) ↔ t
The critical peak s = b(c(b(x1_1))) _{1}←b(c(c(x1_1)))→_ε a(c(c(x1_1))) = t can be joined as follows.
s ↔ a(c(b(x1_1))) ↔ t
The critical peak s = b(c(c(x1_1))) _{1}←b(c(c(x1_1)))→_ε a(c(c(x1_1))) = t can be joined as follows.
s ↔ t
The critical peak s = b(a(b(x1_1))) _{1}←b(c(b(x1_1)))→_ε a(c(b(x1_1))) = t can be joined as follows.
s ↔ b(a(c(x1_1))) ↔ b(c(b(x1_1))) ↔ t
The critical peak s = c(a(c(x1_1))) _{1}←c(b(c(x1_1)))→_ε a(b(c(x1_1))) = t can be joined as follows.
s ↔ c(b(c(x1_1))) ↔ a(c(c(x1_1))) ↔ t

The TRS C is chosen as:

a(b(x))	→	a(c(x))
c(c(x))	→	c(b(x))
a(c(x))	→	c(b(x))
b(c(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

The critical peak s = a(a(c(x1_1))) _{1}←a(b(c(x1_1)))→_ε a(c(c(x1_1))) = t can be joined as follows.
s ↔ a(c(b(x1_1))) ↔ t
The critical peak s = c(c(b(x1_1))) _{1}←c(c(c(x1_1)))→_ε c(b(c(x1_1))) = t can be joined as follows.
s ↔ c(a(c(x1_1))) ↔ t
The critical peak s = a(c(b(x1_1))) _{1}←a(c(c(x1_1)))→_ε c(b(c(x1_1))) = t can be joined as follows.
s ↔ c(b(b(x1_1))) ↔ c(c(b(x1_1))) ↔ c(a(c(x1_1))) ↔ t
The critical peak s = b(c(b(x1_1))) _{1}←b(c(c(x1_1)))→_ε a(c(c(x1_1))) = t can be joined as follows.
s ↔ a(c(b(x1_1))) ↔ t

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(b(c(x1_1)))	→	a(a(c(x1_1)))
a(b(c(x1_1)))	→	a(c(c(x1_1)))
c(c(c(x1_1)))	→	c(c(b(x1_1)))
c(c(c(x1_1)))	→	c(b(c(x1_1)))
a(c(c(x1_1)))	→	a(c(b(x1_1)))
a(c(c(x1_1)))	→	c(b(c(x1_1)))
b(c(c(x1_1)))	→	b(c(b(x1_1)))
b(c(c(x1_1)))	→	a(c(c(x1_1)))

Relative termination of P / R is proven as follows.

1.2.1 Rule Removal

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the naturals

[b(x₁)]

1	0
0	0

· x₁ +

0	0
2	0

[c(x₁)]

1	0
0	0

· x₁ +

0	0
0	0

[a(x₁)]

1	2
0	1

· x₁ +

0	0
2	0

the rules

a(b(c(x1_1)))	→	a(a(c(x1_1)))
c(c(c(x1_1)))	→	c(c(b(x1_1)))
c(c(c(x1_1)))	→	c(b(c(x1_1)))
a(c(c(x1_1)))	→	a(c(b(x1_1)))
a(c(c(x1_1)))	→	c(b(c(x1_1)))
b(c(c(x1_1)))	→	b(c(b(x1_1)))
b(c(c(x1_1)))	→	a(c(c(x1_1)))

remain in R. Moreover, the rules

c(c(x))	→	c(b(x))
a(c(x))	→	c(b(x))
b(c(x))	→	a(c(x))

remain in S.

1.2.1.1 Rule Removal

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the naturals

[b(x₁)]

1	0
1	0

· x₁ +

0	0
2	0

[c(x₁)]

1	0
1	0

· x₁ +

2	0
0	0

[a(x₁)]

1	0
0	1

· x₁ +

0	0
1	0

the rules

a(b(c(x1_1)))	→	a(a(c(x1_1)))
a(c(c(x1_1)))	→	c(b(c(x1_1)))
b(c(c(x1_1)))	→	a(c(c(x1_1)))

remain in R. Moreover, the rules

a(c(x))	→	c(b(x))
b(c(x))	→	a(c(x))

remain in S.

1.2.1.1.1 Rule Removal

Using the recursive path order with the following precedence and status

prec(a)	=	1	stat(a)	=	lex
prec(b)	=	1	stat(b)	=	lex
prec(c)	=	0	stat(c)	=	lex

the rules

a(b(c(x1_1)))	→	a(a(c(x1_1)))
b(c(c(x1_1)))	→	a(c(c(x1_1)))

remain in R. Moreover, the rule

b(c(x))

→

a(c(x))

remains in S.

1.2.1.1.1.1 Rule Removal

Using the recursive path order with the following precedence and status

prec(a)	=	0	stat(a)	=	lex
prec(b)	=	1	stat(b)	=	lex
prec(c)	=	0	stat(c)	=	lex

all rules of R could be removed. Moreover, all rules of S could be removed.

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

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

Tool configuration

Hakusan

version: 0.10