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

The TRS C is chosen as:

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))

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 Rule Labeling with Parallel Critical Pairs

Confluence is proven by compositional rule labeling with parallel critical pairs.
The following labeling functions phi and psi are used (if only one is displayed, then phi = psi).

- a(c(x))→b(a(x)) ↦ 2
- a(c(x))→a(c(x)) ↦ 1
- a(a(x))→a(b(x)) ↦ 3
- b(b(x))→a(c(x)) ↦ 8
- c(c(x))→c(a(x)) ↦ 10
- c(b(x))→a(c(x)) ↦ 12
- a(b(x))→a(c(x)) ↦ 4
- a(c(x))→a(c(x)) ↦ 0
- a(c(x))→b(a(x)) ↦ 7
- a(c(x))→a(c(x)) ↦ 3
- a(a(x))→a(b(x)) ↦ 9
- b(b(x))→a(c(x)) ↦ 11
- c(c(x))→c(a(x)) ↦ 6
- c(b(x))→a(c(x)) ↦ 5
- a(b(x))→a(c(x)) ↦ 6
- a(c(x))→a(c(x)) ↦ 0

The non-0-0 parallel critical pairs are joined as follows.

The parallel-phi-root-psi 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(c(y1)) _{ε}←₁ a(c(y1)) ₇→_ε b(a(y1)) = t can be joined as follows.
  s ↔ b(a(y1)) ↔ t
- The critical peak s = a(c(a(x1_1))) _{1}←₁₀ a(c(c(x1_1))) ₇→_ε b(a(c(x1_1))) = t can be joined as follows.
  s ↔ b(a(a(x1_1))) ↔ b(a(b(x1_1))) ↔ b(a(c(x1_1))) ↔ b(a(b(x1_1))) ↔ b(a(a(x1_1))) ↔ a(c(a(x1_1))) ↔ b(b(a(x1_1))) ↔ t
- The critical peak s = a(a(c(x1_1))) _{1}←₁₂ a(c(b(x1_1))) ₇→_ε b(a(b(x1_1))) = t can be joined as follows.
  s ↔ a(b(c(x1_1))) ↔ a(c(c(x1_1))) ↔ a(c(a(x1_1))) ↔ b(b(a(x1_1))) ↔ b(a(c(x1_1))) ↔ t
- The critical peak s = b(a(y1)) _{ε}←₂ a(c(y1)) ₃→_ε a(c(y1)) = t can be joined as follows.
  s ↔ b(a(y1)) ↔ a(c(y1)) ↔ t
- The critical peak s = a(c(a(x1_1))) _{1}←₁₀ a(c(c(x1_1))) ₃→_ε a(c(c(x1_1))) = t can be joined as follows.
  s ↔ b(a(a(x1_1))) ↔ b(a(b(x1_1))) ↔ b(a(c(x1_1))) ↔ b(b(a(x1_1))) ↔ b(a(c(x1_1))) ↔ a(c(c(x1_1))) ↔ t
- The critical peak s = a(a(c(x1_1))) _{1}←₁₂ a(c(b(x1_1))) ₃→_ε a(c(b(x1_1))) = t can be joined as follows.
  s ↔ a(a(c(x1_1))) ↔ a(b(c(x1_1))) ↔ a(c(c(x1_1))) ↔ a(c(a(x1_1))) ↔ b(b(a(x1_1))) ↔ b(a(c(x1_1))) ↔ b(a(b(x1_1))) ↔ a(c(b(x1_1))) ↔ t
- The critical peak s = a(b(a(x1_1))) _{1}←₂ a(a(c(x1_1))) ₉→_ε a(b(c(x1_1))) = t can be joined as follows.
  s ↔ a(c(a(x1_1))) ↔ b(b(a(x1_1))) ↔ b(a(c(x1_1))) ↔ a(c(c(x1_1))) ↔ t
- The critical peak s = a(a(c(x1_1))) _{1}←₁ a(a(c(x1_1))) ₉→_ε a(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(a(a(x1_1))) ₉→_ε a(b(a(x1_1))) = t can be joined as follows.
  s ↔ a(b(b(x1_1))) ↔ a(c(b(x1_1))) ↔ b(a(b(x1_1))) ↔ b(a(c(x1_1))) ↔ b(b(a(x1_1))) ↔ b(a(c(x1_1))) ↔ b(a(b(x1_1))) ↔ b(a(a(x1_1))) ↔ a(c(a(x1_1))) ↔ t
- The critical peak s = a(a(c(x1_1))) _{1}←₄ a(a(b(x1_1))) ₉→_ε a(b(b(x1_1))) = t can be joined as follows.
  s ↔ a(a(c(x1_1))) ↔ a(b(a(x1_1))) ↔ a(c(a(x1_1))) ↔ b(a(a(x1_1))) ↔ a(c(a(x1_1))) ↔ a(b(a(x1_1))) ↔ a(a(c(x1_1))) ↔ a(b(b(x1_1))) ↔ t
- The critical peak s = b(a(c(x1_1))) _{1}←₈ b(b(b(x1_1))) ₁₁→_ε a(c(b(x1_1))) = t can be joined as follows.
  s ↔ b(a(c(x1_1))) ↔ b(b(a(x1_1))) ↔ b(a(c(x1_1))) ↔ b(a(b(x1_1))) ↔ t
- The critical peak s = c(c(a(x1_1))) _{1}←₁₀ c(c(c(x1_1))) ₆→_ε c(a(c(x1_1))) = t can be joined as follows.
  s ↔ c(a(a(x1_1))) ↔ c(a(b(x1_1))) ↔ c(a(c(x1_1))) ↔ t
- The critical peak s = c(a(c(x1_1))) _{1}←₁₂ c(c(b(x1_1))) ₆→_ε c(a(b(x1_1))) = t can be joined as follows.
  s ↔ c(a(c(x1_1))) ↔ c(a(b(x1_1))) ↔ t
- The critical peak s = c(a(c(x1_1))) _{1}←₈ c(b(b(x1_1))) ₅→_ε a(c(b(x1_1))) = t can be joined as follows.
  s ↔ c(a(c(x1_1))) ↔ c(b(a(x1_1))) ↔ a(c(a(x1_1))) ↔ b(b(a(x1_1))) ↔ b(a(c(x1_1))) ↔ b(a(b(x1_1))) ↔ t
- The critical peak s = a(a(c(x1_1))) _{1}←₈ a(b(b(x1_1))) ₆→_ε a(c(b(x1_1))) = t can be joined as follows.
  s ↔ a(a(c(x1_1))) ↔ a(b(a(x1_1))) ↔ a(c(a(x1_1))) ↔ b(a(a(x1_1))) ↔ a(c(a(x1_1))) ↔ b(b(a(x1_1))) ↔ b(a(c(x1_1))) ↔ b(a(b(x1_1))) ↔ t
The parallel-psi-root-phi 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(c(y1)) _{ε}←₃ a(c(y1)) ₂→_ε b(a(y1)) = t can be joined as follows.
  s ↔ b(a(y1)) ↔ t
- The critical peak s = a(c(a(x1_1))) _{1}←₆ a(c(c(x1_1))) ₂→_ε b(a(c(x1_1))) = t can be joined as follows.
  s ↔ a(c(a(x1_1))) ↔ b(a(a(x1_1))) ↔ b(a(b(x1_1))) ↔ b(a(c(x1_1))) ↔ t
- The critical peak s = a(a(c(x1_1))) _{1}←₅ a(c(b(x1_1))) ₂→_ε b(a(b(x1_1))) = t can be joined as follows.
  s ↔ a(b(a(x1_1))) ↔ a(c(a(x1_1))) ↔ b(a(a(x1_1))) ↔ b(a(b(x1_1))) ↔ t
- The critical peak s = b(a(y1)) _{ε}←₇ a(c(y1)) ₁→_ε a(c(y1)) = t can be joined as follows.
  s ↔ b(a(y1)) ↔ t
- The critical peak s = a(c(a(x1_1))) _{1}←₆ a(c(c(x1_1))) ₁→_ε a(c(c(x1_1))) = t can be joined as follows.
  s ↔ a(c(a(x1_1))) ↔ t
- The critical peak s = a(a(c(x1_1))) _{1}←₅ a(c(b(x1_1))) ₁→_ε a(c(b(x1_1))) = t can be joined as follows.
  s ↔ a(a(c(x1_1))) ↔ t
- The critical peak s = a(b(a(x1_1))) _{1}←₇ a(a(c(x1_1))) ₃→_ε a(b(c(x1_1))) = t can be joined as follows.
  s ↔ a(c(a(x1_1))) ↔ a(c(c(x1_1))) ↔ a(b(c(x1_1))) ↔ t
- The critical peak s = a(a(c(x1_1))) _{1}←₃ a(a(c(x1_1))) ₃→_ε a(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(a(a(x1_1))) ₃→_ε a(b(a(x1_1))) = t can be joined as follows.
  s ↔ a(b(b(x1_1))) ↔ a(a(c(x1_1))) ↔ a(b(a(x1_1))) ↔ a(c(a(x1_1))) ↔ a(b(a(x1_1))) ↔ t
- The critical peak s = a(a(c(x1_1))) _{1}←₆ a(a(b(x1_1))) ₃→_ε a(b(b(x1_1))) = t can be joined as follows.
  s ↔ a(a(c(x1_1))) ↔ a(c(b(x1_1))) ↔ t
- The critical peak s = b(a(c(x1_1))) _{1}←₁₁ b(b(b(x1_1))) ₈→_ε a(c(b(x1_1))) = t can be joined as follows.
  s ↔ b(b(a(x1_1))) ↔ a(c(a(x1_1))) ↔ b(a(a(x1_1))) ↔ a(c(a(x1_1))) ↔ a(c(c(x1_1))) ↔ a(b(c(x1_1))) ↔ a(a(c(x1_1))) ↔ t
- The critical peak s = c(c(a(x1_1))) _{1}←₆ c(c(c(x1_1))) ₁₀→_ε c(a(c(x1_1))) = t can be joined as follows.
  s ↔ c(a(a(x1_1))) ↔ c(a(b(x1_1))) ↔ c(a(c(x1_1))) ↔ t
- The critical peak s = c(a(c(x1_1))) _{1}←₅ c(c(b(x1_1))) ₁₀→_ε c(a(b(x1_1))) = t can be joined as follows.
  s ↔ c(a(c(x1_1))) ↔ c(a(b(x1_1))) ↔ t
- The critical peak s = c(a(c(x1_1))) _{1}←₁₁ c(b(b(x1_1))) ₁₂→_ε a(c(b(x1_1))) = t can be joined as follows.
  s ↔ c(b(a(x1_1))) ↔ a(c(a(x1_1))) ↔ b(a(a(x1_1))) ↔ b(a(b(x1_1))) ↔ b(a(c(x1_1))) ↔ a(c(c(x1_1))) ↔ a(b(c(x1_1))) ↔ a(a(c(x1_1))) ↔ t
- The critical peak s = a(a(c(x1_1))) _{1}←₁₁ a(b(b(x1_1))) ₄→_ε a(c(b(x1_1))) = t can be joined as follows.
  s ↔ a(b(c(x1_1))) ↔ a(c(c(x1_1))) ↔ a(c(a(x1_1))) ↔ b(a(a(x1_1))) ↔ a(c(a(x1_1))) ↔ a(c(c(x1_1))) ↔ a(b(c(x1_1))) ↔ a(a(c(x1_1))) ↔ t

The remaining rules are handled recursively.

There are no rules.

1.2.1 (Weakly) Orthogonal

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

Tool configuration

Hakusan

version: 0.10