Certification Problem
Input (COPS 1012)
We consider the TRS containing the following rules:
|
c(c(x)) |
→ |
a(c(x)) |
(1) |
|
c(b(x)) |
→ |
c(c(x)) |
(2) |
|
b(a(x)) |
→ |
c(b(x)) |
(3) |
|
a(b(x)) |
→ |
b(a(x)) |
(4) |
|
c(a(x)) |
→ |
c(a(x)) |
(5) |
|
b(c(x)) |
→ |
c(c(x)) |
(6) |
|
c(c(x)) |
→ |
b(c(x)) |
(7) |
|
c(a(x)) |
→ |
b(c(x)) |
(8) |
The underlying signature is as follows:
{c/1, a/1, b/1}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by csi @ CoCo 2020)
1 Redundant Rules Transformation
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following
modified system:
|
c(a(x)) |
→ |
b(c(x)) |
(8) |
|
c(c(x)) |
→ |
b(c(x)) |
(7) |
|
b(c(x)) |
→ |
c(c(x)) |
(6) |
|
a(b(x)) |
→ |
b(a(x)) |
(4) |
|
b(a(x)) |
→ |
c(b(x)) |
(3) |
|
c(b(x)) |
→ |
c(c(x)) |
(2) |
|
c(c(x)) |
→ |
a(c(x)) |
(1) |
All redundant rules that were added or removed can be
simulated in 1 steps
.
1.1 Redundant Rules Transformation
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following
modified system:
|
c(a(x)) |
→ |
b(c(x)) |
(8) |
|
c(c(x)) |
→ |
b(c(x)) |
(7) |
|
b(c(x)) |
→ |
c(c(x)) |
(6) |
|
a(b(x)) |
→ |
b(a(x)) |
(4) |
|
b(a(x)) |
→ |
c(b(x)) |
(3) |
|
c(b(x)) |
→ |
c(c(x)) |
(2) |
|
c(c(x)) |
→ |
a(c(x)) |
(1) |
|
c(a(x)) |
→ |
c(c(x)) |
(9) |
|
c(c(x)) |
→ |
c(c(x)) |
(10) |
|
b(c(x)) |
→ |
b(c(x)) |
(11) |
|
b(c(x)) |
→ |
a(c(x)) |
(12) |
|
a(b(x)) |
→ |
c(b(x)) |
(13) |
|
b(a(x)) |
→ |
c(c(x)) |
(14) |
|
c(b(x)) |
→ |
b(c(x)) |
(15) |
|
c(b(x)) |
→ |
a(c(x)) |
(16) |
All redundant rules that were added or removed can be
simulated in 2 steps
.
1.1.1 Decreasing Diagrams
1.1.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).
-
↦ 2
-
↦ 4
-
↦ 1
-
↦ 4
-
↦ 0
-
↦ 0
-
↦ 1
-
↦ 0
-
↦ 1
-
↦ 1
-
↦ 1
-
↦ 2
-
↦ 0
-
↦ 4
-
↦ 1
The 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 = c(b(c(x569)))←→ε b(c(a(x569))) = t can be joined as follows.
s
↔ b(c(c(x569))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(b(c(x570))) ↔ b(c(a(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(c(c(x570))) ↔ c(b(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(c(c(x570))) ↔ b(c(a(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(c(c(x570))) ↔ c(c(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(c(c(x570))) ↔ b(c(c(x570))) ↔ c(b(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(c(c(x570))) ↔ b(c(c(x570))) ↔ b(c(a(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(c(c(x570))) ↔ b(c(c(x570))) ↔ c(c(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(c(c(x570))) ↔ c(c(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(c(c(x570))) ↔ c(c(c(x570))) ↔ c(b(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(c(c(x570))) ↔ c(c(c(x570))) ↔ c(c(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(a(c(x570))) ↔ c(c(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(a(c(x570))) ↔ c(c(c(x570))) ↔ c(b(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(a(c(x570))) ↔ c(c(c(x570))) ↔ c(c(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(c(c(x570))) ↔ a(c(c(x570))) ↔ c(b(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(c(c(x570))) ↔ a(c(c(x570))) ↔ a(c(a(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(c(c(x570))) ↔ a(c(c(x570))) ↔ c(c(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(a(c(x570))) ↔ c(b(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(a(c(x570))) ↔ c(b(c(x570))) ↔ c(b(c(x570))) ↔
t
-
The critical peak s = b(b(c(x570)))←→ε c(c(a(x570))) = t can be joined as follows.
s
↔ b(a(c(x570))) ↔ c(b(c(x570))) ↔ c(c(c(x570))) ↔
t
-
The critical peak s = c(b(c(x571)))←→ε a(c(a(x571))) = t can be joined as follows.
s
↔ a(c(c(x571))) ↔
t
-
The critical peak s = b(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔ b(c(x)) ↔
t
-
The critical peak s = b(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = c(b(c(x573)))←→ε c(c(a(x573))) = t can be joined as follows.
s
↔ c(b(c(x573))) ↔
t
-
The critical peak s = c(b(c(x573)))←→ε c(c(a(x573))) = t can be joined as follows.
s
↔ c(c(c(x573))) ↔
t
-
The critical peak s = b(b(c(x574)))←→ε b(c(a(x574))) = t can be joined as follows.
s
↔ b(b(c(x574))) ↔
t
-
The critical peak s = b(b(c(x574)))←→ε b(c(a(x574))) = t can be joined as follows.
s
↔ b(c(c(x574))) ↔
t
-
The critical peak s = b(b(c(x575)))←→ε a(c(a(x575))) = t can be joined as follows.
s
↔ b(a(c(x575))) ↔ a(b(c(x575))) ↔
t
-
The critical peak s = b(b(c(x575)))←→ε a(c(a(x575))) = t can be joined as follows.
s
↔ b(c(c(x575))) ↔ b(a(c(x575))) ↔ a(b(c(x575))) ↔
t
-
The critical peak s = b(b(c(x575)))←→ε a(c(a(x575))) = t can be joined as follows.
s
↔ b(c(c(x575))) ↔ a(c(c(x575))) ↔
t
-
The critical peak s = b(b(c(x575)))←→ε a(c(a(x575))) = t can be joined as follows.
s
↔ b(c(c(x575))) ↔ a(c(c(x575))) ↔ a(b(c(x575))) ↔
t
-
The critical peak s = b(b(c(x575)))←→ε a(c(a(x575))) = t can be joined as follows.
s
↔ b(c(c(x575))) ↔ a(c(c(x575))) ↔ a(c(c(x575))) ↔
t
-
The critical peak s = b(b(c(x575)))←→ε a(c(a(x575))) = t can be joined as follows.
s
↔ b(a(c(x575))) ↔ c(b(c(x575))) ↔ a(b(c(x575))) ↔
t
-
The critical peak s = c(b(c(x576)))←→ε b(c(c(x576))) = t can be joined as follows.
s
↔ c(c(c(x576))) ↔
t
-
The critical peak s = c(b(c(x576)))←→ε b(c(c(x576))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(b(c(x576)))←→ε b(c(c(x576))) = t can be joined as follows.
s
↔ a(c(c(x576))) ↔
t
-
The critical peak s = b(b(c(x577)))←→ε c(c(c(x577))) = t can be joined as follows.
s
↔ b(c(c(x577))) ↔
t
-
The critical peak s = b(c(x))←→ε a(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(b(c(x579)))←→ε a(c(c(x579))) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔ b(c(x)) ↔
t
-
The critical peak s = b(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = c(b(c(x581)))←→ε c(c(c(x581))) = t can be joined as follows.
s
↔ c(b(c(x581))) ↔
t
-
The critical peak s = c(b(c(x581)))←→ε c(c(c(x581))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(b(c(x581)))←→ε c(c(c(x581))) = t can be joined as follows.
s
↔ c(a(c(x581))) ↔
t
-
The critical peak s = c(b(c(x581)))←→ε c(c(c(x581))) = t can be joined as follows.
s
↔ b(c(c(x581))) ↔
t
-
The critical peak s = c(b(c(x581)))←→ε c(c(c(x581))) = t can be joined as follows.
s
↔ a(c(c(x581))) ↔
t
-
The critical peak s = b(b(c(x582)))←→ε b(c(c(x582))) = t can be joined as follows.
s
↔ b(b(c(x582))) ↔
t
-
The critical peak s = b(b(c(x582)))←→ε b(c(c(x582))) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(b(c(x582)))←→ε b(c(c(x582))) = t can be joined as follows.
s
↔ b(a(c(x582))) ↔
t
-
The critical peak s = b(b(c(x583)))←→ε a(c(c(x583))) = t can be joined as follows.
s
↔ b(a(c(x583))) ↔ a(b(c(x583))) ↔
t
-
The critical peak s = b(b(c(x583)))←→ε a(c(c(x583))) = t can be joined as follows.
s
↔ b(c(c(x583))) ↔ b(a(c(x583))) ↔ a(b(c(x583))) ↔
t
-
The critical peak s = b(b(c(x583)))←→ε a(c(c(x583))) = t can be joined as follows.
s
↔ b(c(c(x583))) ↔
t
-
The critical peak s = b(b(c(x583)))←→ε a(c(c(x583))) = t can be joined as follows.
s
↔ b(a(c(x583))) ↔ c(b(c(x583))) ↔ a(b(c(x583))) ↔
t
-
The critical peak s = a(c(c(x584)))←→ε b(a(c(x584))) = t can be joined as follows.
s
↔ a(c(c(x584))) ↔ c(b(c(x584))) ↔
t
-
The critical peak s = a(c(c(x584)))←→ε b(a(c(x584))) = t can be joined as follows.
s
↔ a(c(c(x584))) ↔ c(c(c(x584))) ↔
t
-
The critical peak s = a(c(c(x584)))←→ε b(a(c(x584))) = t can be joined as follows.
s
↔ a(b(c(x584))) ↔
t
-
The critical peak s = a(c(c(x584)))←→ε b(a(c(x584))) = t can be joined as follows.
s
↔ a(b(c(x584))) ↔ c(b(c(x584))) ↔
t
-
The critical peak s = a(c(c(x584)))←→ε b(a(c(x584))) = t can be joined as follows.
s
↔ a(b(c(x584))) ↔ c(b(c(x584))) ↔ c(b(c(x584))) ↔
t
-
The critical peak s = a(c(c(x584)))←→ε b(a(c(x584))) = t can be joined as follows.
s
↔ a(b(c(x584))) ↔ c(b(c(x584))) ↔ c(c(c(x584))) ↔
t
-
The critical peak s = c(c(c(x585)))←→ε c(c(c(x585))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔ c(c(x)) ↔
t
-
The critical peak s = c(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = c(c(x))←→ε a(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = a(c(c(x588)))←→ε c(b(c(x588))) = t can be joined as follows.
s
↔ a(c(c(x588))) ↔
t
-
The critical peak s = c(c(c(x589)))←→ε b(c(c(x589))) = t can be joined as follows.
s
↔ c(c(c(x589))) ↔
t
-
The critical peak s = c(c(c(x589)))←→ε b(c(c(x589))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(c(c(x589)))←→ε b(c(c(x589))) = t can be joined as follows.
s
↔ a(c(c(x589))) ↔
t
-
The critical peak s = c(c(c(x590)))←→ε a(c(c(x590))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(b(a(x591)))←→ε b(c(b(x591))) = t can be joined as follows.
s
↔ c(c(b(x591))) ↔
t
-
The critical peak s = b(b(a(x592)))←→ε c(b(b(x592))) = t can be joined as follows.
s
↔ b(c(b(x592))) ↔
t
-
The critical peak s = c(b(a(x593)))←→ε c(c(b(x593))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(b(a(x593)))←→ε c(c(b(x593))) = t can be joined as follows.
s
↔ c(c(c(x593))) ↔
t
-
The critical peak s = b(a(x))←→ε c(b(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(a(x))←→ε c(b(x)) = t can be joined as follows.
s
↔ c(c(x)) ↔
t
-
The critical peak s = b(b(a(x595)))←→ε c(c(b(x595))) = t can be joined as follows.
s
↔ b(c(b(x595))) ↔
t
-
The critical peak s = a(c(b(x596)))←→ε b(a(a(x596))) = t can be joined as follows.
s
↔ a(b(c(x596))) ↔ c(b(c(x596))) ↔ c(c(a(x596))) ↔
t
-
The critical peak s = c(c(b(x597)))←→ε c(c(a(x597))) = t can be joined as follows.
s
↔ c(c(c(x597))) ↔
t
-
The critical peak s = c(c(b(x597)))←→ε c(c(a(x597))) = t can be joined as follows.
s
↔ c(b(c(x597))) ↔
t
-
The critical peak s = a(c(b(x598)))←→ε c(b(a(x598))) = t can be joined as follows.
s
↔ a(c(b(x598))) ↔ c(c(b(x598))) ↔
t
-
The critical peak s = a(c(b(x598)))←→ε c(b(a(x598))) = t can be joined as follows.
s
↔ a(c(c(x598))) ↔ c(c(c(x598))) ↔
t
-
The critical peak s = a(c(b(x598)))←→ε c(b(a(x598))) = t can be joined as follows.
s
↔ a(c(c(x598))) ↔ a(c(a(x598))) ↔
t
-
The critical peak s = a(c(b(x598)))←→ε c(b(a(x598))) = t can be joined as follows.
s
↔ a(c(c(x598))) ↔ a(c(c(x598))) ↔ c(c(c(x598))) ↔
t
-
The critical peak s = a(c(b(x598)))←→ε c(b(a(x598))) = t can be joined as follows.
s
↔ a(c(c(x598))) ↔ a(c(c(x598))) ↔ a(c(a(x598))) ↔
t
-
The critical peak s = a(c(b(x598)))←→ε c(b(a(x598))) = t can be joined as follows.
s
↔ a(b(c(x598))) ↔ a(c(c(x598))) ↔ c(c(c(x598))) ↔
t
-
The critical peak s = a(c(b(x598)))←→ε c(b(a(x598))) = t can be joined as follows.
s
↔ a(b(c(x598))) ↔ a(c(c(x598))) ↔ a(c(a(x598))) ↔
t
-
The critical peak s = a(c(b(x598)))←→ε c(b(a(x598))) = t can be joined as follows.
s
↔ a(b(c(x598))) ↔ a(c(a(x598))) ↔
t
-
The critical peak s = a(c(b(x598)))←→ε c(b(a(x598))) = t can be joined as follows.
s
↔ a(c(c(x598))) ↔ a(b(c(x598))) ↔ a(c(a(x598))) ↔
t
-
The critical peak s = a(c(b(x598)))←→ε c(b(a(x598))) = t can be joined as follows.
s
↔ a(b(c(x598))) ↔ a(b(c(x598))) ↔ a(c(a(x598))) ↔
t
-
The critical peak s = a(c(b(x598)))←→ε c(b(a(x598))) = t can be joined as follows.
s
↔ a(b(c(x598))) ↔ c(b(c(x598))) ↔ c(c(b(x598))) ↔
t
-
The critical peak s = a(c(b(x598)))←→ε c(b(a(x598))) = t can be joined as follows.
s
↔ a(b(c(x598))) ↔ c(b(c(x598))) ↔ c(c(a(x598))) ↔
t
-
The critical peak s = a(c(b(x598)))←→ε c(b(a(x598))) = t can be joined as follows.
s
↔ a(b(c(x598))) ↔ c(b(c(x598))) ↔ c(c(c(x598))) ↔
t
-
The critical peak s = c(b(x))←→ε c(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(b(x))←→ε c(c(x)) = t can be joined as follows.
s
↔ b(c(x)) ↔
t
-
The critical peak s = c(b(x))←→ε c(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(c(c(x600))) ↔ c(c(a(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(c(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(c(c(x600))) ↔ c(c(c(x600))) ↔ c(c(a(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(c(c(x600))) ↔ c(c(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(b(c(x600))) ↔ c(c(c(x600))) ↔ c(c(a(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(b(c(x600))) ↔ c(c(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(a(c(x600))) ↔ c(c(c(x600))) ↔ c(c(a(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(a(c(x600))) ↔ c(c(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(b(c(x600))) ↔ c(c(a(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(c(c(x600))) ↔ c(b(c(x600))) ↔ c(c(a(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(b(c(x600))) ↔ c(b(c(x600))) ↔ c(c(a(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ b(c(b(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ b(c(b(x600))) ↔ b(c(c(x600))) ↔ b(b(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ b(c(b(x600))) ↔ b(c(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(c(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(c(c(x600))) ↔ b(c(c(x600))) ↔ b(b(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(c(c(x600))) ↔ b(c(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(b(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(b(c(x600))) ↔ b(c(c(x600))) ↔ b(b(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(b(c(x600))) ↔ b(c(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(a(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(a(c(x600))) ↔ b(c(c(x600))) ↔ b(b(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(a(c(x600))) ↔ b(c(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ b(c(b(x600))) ↔ b(b(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ b(c(b(x600))) ↔ b(b(c(x600))) ↔ b(b(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ b(c(b(x600))) ↔ b(b(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ b(c(b(x600))) ↔ b(a(c(x600))) ↔ b(b(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ b(c(b(x600))) ↔ b(a(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(c(c(x600))) ↔ a(c(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(c(c(x600))) ↔ a(c(c(x600))) ↔ a(c(a(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ a(c(b(x600))) ↔ a(c(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ a(c(b(x600))) ↔ a(c(c(x600))) ↔ a(c(a(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(b(c(x600))) ↔ a(c(c(x600))) ↔ b(c(c(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ c(b(c(x600))) ↔ a(c(c(x600))) ↔ a(c(a(x600))) ↔
t
-
The critical peak s = c(c(b(x600)))←→ε b(c(a(x600))) = t can be joined as follows.
s
↔ a(c(b(x600))) ↔ a(b(c(x600))) ↔ a(c(a(x600))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ c(b(c(x601))) ↔ a(b(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ c(c(c(x601))) ↔ c(b(c(x601))) ↔ a(b(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ c(b(c(x601))) ↔ c(b(c(x601))) ↔ a(b(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ b(c(b(x601))) ↔ b(a(c(x601))) ↔ a(b(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ c(c(c(x601))) ↔ a(c(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ c(c(c(x601))) ↔ a(c(c(x601))) ↔ a(b(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ c(c(c(x601))) ↔ a(c(c(x601))) ↔ a(c(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ a(c(b(x601))) ↔ a(c(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ a(c(b(x601))) ↔ a(c(c(x601))) ↔ a(b(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ a(c(b(x601))) ↔ a(c(c(x601))) ↔ a(c(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ c(b(c(x601))) ↔ a(c(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ c(b(c(x601))) ↔ a(c(c(x601))) ↔ a(b(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ c(b(c(x601))) ↔ a(c(c(x601))) ↔ a(c(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ a(c(b(x601))) ↔ a(b(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ a(c(b(x601))) ↔ a(b(c(x601))) ↔ a(b(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ a(c(b(x601))) ↔ a(b(c(x601))) ↔ a(c(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ a(c(b(x601))) ↔ a(a(c(x601))) ↔ a(b(c(x601))) ↔
t
-
The critical peak s = c(c(b(x601)))←→ε a(c(a(x601))) = t can be joined as follows.
s
↔ a(c(b(x601))) ↔ a(a(c(x601))) ↔ a(c(c(x601))) ↔
t
-
The critical peak s = c(c(c(x602)))←→ε b(c(b(x602))) = t can be joined as follows.
s
↔ b(c(c(x602))) ↔
t
-
The critical peak s = b(c(c(x603)))←→ε c(c(b(x603))) = t can be joined as follows.
s
↔ c(c(c(x603))) ↔
t
-
The critical peak s = c(c(c(x604)))←→ε a(c(b(x604))) = t can be joined as follows.
s
↔ a(c(c(x604))) ↔
t
-
The critical peak s = c(c(c(x605)))←→ε c(c(b(x605))) = t can be joined as follows.
s
↔ c(c(c(x605))) ↔
t
-
The critical peak s = c(c(c(x605)))←→ε c(c(b(x605))) = t can be joined as follows.
s
↔ c(b(c(x605))) ↔
t
-
The critical peak s = c(c(c(x605)))←→ε c(c(b(x605))) = t can be joined as follows.
s
↔ c(a(c(x605))) ↔
t
-
The critical peak s = b(c(c(x606)))←→ε b(c(b(x606))) = t can be joined as follows.
s
↔ b(c(c(x606))) ↔
t
-
The critical peak s = b(c(c(x606)))←→ε b(c(b(x606))) = t can be joined as follows.
s
↔ b(b(c(x606))) ↔
t
-
The critical peak s = b(c(c(x606)))←→ε b(c(b(x606))) = t can be joined as follows.
s
↔ b(a(c(x606))) ↔
t
-
The critical peak s = b(c(c(x607)))←→ε a(c(b(x607))) = t can be joined as follows.
s
↔ a(c(c(x607))) ↔
t
-
The critical peak s = c(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔ c(c(x)) ↔
t
-
The critical peak s = c(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = c(c(x))←→ε a(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = a(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = c(a(c(x611)))←→ε b(c(c(x611))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(a(c(x611)))←→ε b(c(c(x611))) = t can be joined as follows.
s
↔ c(c(c(x611))) ↔
t
-
The critical peak s = b(a(c(x612)))←→ε c(c(c(x612))) = t can be joined as follows.
s
↔ c(b(c(x612))) ↔
t
-
The critical peak s = b(a(c(x612)))←→ε c(c(c(x612))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(a(c(x613)))←→ε a(c(c(x613))) = t can be joined as follows.
s
↔ b(c(c(x613))) ↔ b(a(c(x613))) ↔ a(b(c(x613))) ↔
t
-
The critical peak s = c(a(c(x613)))←→ε a(c(c(x613))) = t can be joined as follows.
s
↔ b(c(c(x613))) ↔
t
-
The critical peak s = c(a(c(x613)))←→ε a(c(c(x613))) = t can be joined as follows.
s
↔ c(c(c(x613))) ↔
t
-
The critical peak s = c(a(c(x613)))←→ε a(c(c(x613))) = t can be joined as follows.
s
↔ c(c(c(x613))) ↔ c(b(c(x613))) ↔ a(b(c(x613))) ↔
t
-
The critical peak s = a(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = c(a(c(x615)))←→ε c(c(c(x615))) = t can be joined as follows.
s
↔ c(a(c(x615))) ↔
t
-
The critical peak s = c(a(c(x615)))←→ε c(c(c(x615))) = t can be joined as follows.
s
↔ b(c(c(x615))) ↔
t
-
The critical peak s = c(a(c(x615)))←→ε c(c(c(x615))) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(a(c(x616)))←→ε b(c(c(x616))) = t can be joined as follows.
s
↔ b(a(c(x616))) ↔
t
-
The critical peak s = b(a(c(x616)))←→ε b(c(c(x616))) = t can be joined as follows.
s
↔ c(c(c(x616))) ↔
t
-
The critical peak s = b(a(c(x617)))←→ε a(c(c(x617))) = t can be joined as follows.
s
↔ b(a(c(x617))) ↔ a(b(c(x617))) ↔
t
-
The critical peak s = b(a(c(x617)))←→ε a(c(c(x617))) = t can be joined as follows.
s
↔ c(b(c(x617))) ↔ a(b(c(x617))) ↔
t
-
The critical peak s = b(a(c(x617)))←→ε a(c(c(x617))) = t can be joined as follows.
s
↔ c(b(c(x617))) ↔ c(b(c(x617))) ↔ a(b(c(x617))) ↔
t
-
The critical peak s = b(a(c(x617)))←→ε a(c(c(x617))) = t can be joined as follows.
s
↔ c(c(c(x617))) ↔ c(b(c(x617))) ↔ a(b(c(x617))) ↔
t
-
The critical peak s = b(a(c(x617)))←→ε a(c(c(x617))) = t can be joined as follows.
s
↔ c(b(c(x617))) ↔
t
-
The critical peak s = b(a(c(x617)))←→ε a(c(c(x617))) = t can be joined as follows.
s
↔ c(c(c(x617))) ↔
t
-
The critical peak s = c(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔ c(c(x)) ↔
t
-
The critical peak s = c(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = c(c(c(x619)))←→ε b(c(a(x619))) = t can be joined as follows.
s
↔ b(c(c(x619))) ↔
t
-
The critical peak s = b(c(c(x620)))←→ε c(c(a(x620))) = t can be joined as follows.
s
↔ c(c(c(x620))) ↔
t
-
The critical peak s = c(c(c(x621)))←→ε a(c(a(x621))) = t can be joined as follows.
s
↔ a(c(c(x621))) ↔
t
-
The critical peak s = c(c(c(x622)))←→ε c(c(a(x622))) = t can be joined as follows.
s
↔ c(c(c(x622))) ↔
t
-
The critical peak s = c(c(c(x622)))←→ε c(c(a(x622))) = t can be joined as follows.
s
↔ c(b(c(x622))) ↔
t
-
The critical peak s = b(c(c(x623)))←→ε b(c(a(x623))) = t can be joined as follows.
s
↔ b(c(c(x623))) ↔
t
-
The critical peak s = b(c(c(x623)))←→ε b(c(a(x623))) = t can be joined as follows.
s
↔ b(b(c(x623))) ↔
t
-
The critical peak s = b(c(c(x624)))←→ε a(c(a(x624))) = t can be joined as follows.
s
↔ a(c(c(x624))) ↔
t
-
The critical peak s = c(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔ c(c(x)) ↔
t
-
The critical peak s = c(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = c(c(c(x626)))←→ε b(c(c(x626))) = t can be joined as follows.
s
↔ c(c(c(x626))) ↔
t
-
The critical peak s = c(c(c(x626)))←→ε b(c(c(x626))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(c(c(x626)))←→ε b(c(c(x626))) = t can be joined as follows.
s
↔ a(c(c(x626))) ↔
t
-
The critical peak s = b(c(c(x627)))←→ε c(c(c(x627))) = t can be joined as follows.
s
↔ b(c(c(x627))) ↔
t
-
The critical peak s = b(c(c(x627)))←→ε c(c(c(x627))) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(c(c(x627)))←→ε c(c(c(x627))) = t can be joined as follows.
s
↔ a(c(c(x627))) ↔
t
-
The critical peak s = c(c(x))←→ε a(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(c(c(x629)))←→ε a(c(c(x629))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(c(c(x630)))←→ε c(c(c(x630))) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(c(c(x631)))←→ε b(c(c(x631))) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(c(c(x632)))←→ε a(c(c(x632))) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔ b(c(x)) ↔
t
-
The critical peak s = b(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = a(b(c(x634)))←→ε b(a(c(x634))) = t can be joined as follows.
s
↔
t
-
The critical peak s = a(b(c(x634)))←→ε b(a(c(x634))) = t can be joined as follows.
s
↔ c(b(c(x634))) ↔
t
-
The critical peak s = c(b(c(x635)))←→ε c(c(c(x635))) = t can be joined as follows.
s
↔ c(b(c(x635))) ↔
t
-
The critical peak s = c(b(c(x635)))←→ε c(c(c(x635))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(b(c(x635)))←→ε c(c(c(x635))) = t can be joined as follows.
s
↔ c(a(c(x635))) ↔
t
-
The critical peak s = c(b(c(x635)))←→ε c(c(c(x635))) = t can be joined as follows.
s
↔ b(c(c(x635))) ↔
t
-
The critical peak s = c(b(c(x635)))←→ε c(c(c(x635))) = t can be joined as follows.
s
↔ a(c(c(x635))) ↔
t
-
The critical peak s = b(c(x))←→ε a(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = a(b(c(x637)))←→ε c(b(c(x637))) = t can be joined as follows.
s
↔ a(c(c(x637))) ↔
t
-
The critical peak s = a(b(c(x637)))←→ε c(b(c(x637))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(b(c(x638)))←→ε b(c(c(x638))) = t can be joined as follows.
s
↔ c(c(c(x638))) ↔
t
-
The critical peak s = c(b(c(x638)))←→ε b(c(c(x638))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(b(c(x638)))←→ε b(c(c(x638))) = t can be joined as follows.
s
↔ a(c(c(x638))) ↔
t
-
The critical peak s = c(b(c(x639)))←→ε a(c(c(x639))) = t can be joined as follows.
s
↔
t
-
The critical peak s = a(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = a(a(c(x641)))←→ε b(a(c(x641))) = t can be joined as follows.
s
↔ a(a(c(x641))) ↔ a(c(c(x641))) ↔ c(b(c(x641))) ↔
t
-
The critical peak s = a(a(c(x641)))←→ε b(a(c(x641))) = t can be joined as follows.
s
↔ a(a(c(x641))) ↔ a(c(c(x641))) ↔ c(c(c(x641))) ↔
t
-
The critical peak s = c(a(c(x642)))←→ε c(c(c(x642))) = t can be joined as follows.
s
↔ c(a(c(x642))) ↔
t
-
The critical peak s = c(a(c(x642)))←→ε c(c(c(x642))) = t can be joined as follows.
s
↔ b(c(c(x642))) ↔
t
-
The critical peak s = c(a(c(x642)))←→ε c(c(c(x642))) = t can be joined as follows.
s
↔
t
-
The critical peak s = a(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = a(a(c(x644)))←→ε c(b(c(x644))) = t can be joined as follows.
s
↔ a(a(c(x644))) ↔ a(c(c(x644))) ↔
t
-
The critical peak s = c(a(c(x645)))←→ε b(c(c(x645))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(a(c(x645)))←→ε b(c(c(x645))) = t can be joined as follows.
s
↔ c(c(c(x645))) ↔
t
-
The critical peak s = c(a(c(x646)))←→ε a(c(c(x646))) = t can be joined as follows.
s
↔ b(c(c(x646))) ↔ b(a(c(x646))) ↔ a(b(c(x646))) ↔
t
-
The critical peak s = c(a(c(x646)))←→ε a(c(c(x646))) = t can be joined as follows.
s
↔ b(c(c(x646))) ↔
t
-
The critical peak s = c(a(c(x646)))←→ε a(c(c(x646))) = t can be joined as follows.
s
↔ c(c(c(x646))) ↔
t
-
The critical peak s = c(a(c(x646)))←→ε a(c(c(x646))) = t can be joined as follows.
s
↔ c(c(c(x646))) ↔ c(b(c(x646))) ↔ a(b(c(x646))) ↔
t
-
The critical peak s = c(c(b(x647)))←→ε b(c(b(x647))) = t can be joined as follows.
s
↔ c(c(b(x647))) ↔
t
-
The critical peak s = c(c(b(x647)))←→ε b(c(b(x647))) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(c(b(x647)))←→ε b(c(b(x647))) = t can be joined as follows.
s
↔ a(c(b(x647))) ↔
t
-
The critical peak s = c(b(x))←→ε b(a(x)) = t can be joined as follows.
s
↔ c(b(x)) ↔
t
-
The critical peak s = c(b(x))←→ε b(a(x)) = t can be joined as follows.
s
↔ c(c(x)) ↔
t
-
The critical peak s = b(c(b(x649)))←→ε c(b(b(x649))) = t can be joined as follows.
s
↔ b(c(b(x649))) ↔
t
-
The critical peak s = b(c(b(x649)))←→ε c(b(b(x649))) = t can be joined as follows.
s
↔ c(c(b(x649))) ↔
t
-
The critical peak s = b(c(b(x649)))←→ε c(b(b(x649))) = t can be joined as follows.
s
↔ a(c(b(x649))) ↔
t
-
The critical peak s = c(c(b(x650)))←→ε c(c(b(x650))) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(c(b(x651)))←→ε c(c(b(x651))) = t can be joined as follows.
s
↔ b(c(b(x651))) ↔
t
-
The critical peak s = b(c(b(x651)))←→ε c(c(b(x651))) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(c(b(x651)))←→ε c(c(b(x651))) = t can be joined as follows.
s
↔ a(c(b(x651))) ↔
t
-
The critical peak s = a(c(c(x652)))←→ε b(a(a(x652))) = t can be joined as follows.
s
↔ a(b(c(x652))) ↔ c(b(c(x652))) ↔ c(c(a(x652))) ↔
t
-
The critical peak s = c(c(x))←→ε c(b(x)) = t can be joined as follows.
s
↔ c(c(x)) ↔
t
-
The critical peak s = c(c(x))←→ε c(b(x)) = t can be joined as follows.
s
↔ b(c(x)) ↔
t
-
The critical peak s = c(c(x))←→ε c(b(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = c(c(c(x654)))←→ε c(c(a(x654))) = t can be joined as follows.
s
↔ c(c(c(x654))) ↔
t
-
The critical peak s = c(c(c(x654)))←→ε c(c(a(x654))) = t can be joined as follows.
s
↔ c(b(c(x654))) ↔
t
-
The critical peak s = a(c(c(x655)))←→ε c(b(a(x655))) = t can be joined as follows.
s
↔ a(c(c(x655))) ↔ c(c(c(x655))) ↔
t
-
The critical peak s = a(c(c(x655)))←→ε c(b(a(x655))) = t can be joined as follows.
s
↔ a(c(c(x655))) ↔ a(c(a(x655))) ↔
t
-
The critical peak s = a(c(c(x655)))←→ε c(b(a(x655))) = t can be joined as follows.
s
↔ a(b(c(x655))) ↔ a(c(a(x655))) ↔
t
-
The critical peak s = a(c(c(x655)))←→ε c(b(a(x655))) = t can be joined as follows.
s
↔ a(b(c(x655))) ↔ a(b(c(x655))) ↔ a(c(a(x655))) ↔
t
-
The critical peak s = a(c(c(x655)))←→ε c(b(a(x655))) = t can be joined as follows.
s
↔ a(b(c(x655))) ↔ c(b(c(x655))) ↔ c(c(b(x655))) ↔
t
-
The critical peak s = a(c(c(x655)))←→ε c(b(a(x655))) = t can be joined as follows.
s
↔ a(b(c(x655))) ↔ c(b(c(x655))) ↔ c(c(a(x655))) ↔
t
-
The critical peak s = a(c(c(x655)))←→ε c(b(a(x655))) = t can be joined as follows.
s
↔ a(b(c(x655))) ↔ c(b(c(x655))) ↔ c(c(c(x655))) ↔
t
-
The critical peak s = c(c(c(x656)))←→ε b(c(a(x656))) = t can be joined as follows.
s
↔ b(c(c(x656))) ↔
t
-
The critical peak s = c(c(c(x657)))←→ε a(c(a(x657))) = t can be joined as follows.
s
↔ a(c(c(x657))) ↔
t
-
The critical peak s = c(b(c(x658)))←→ε b(c(b(x658))) = t can be joined as follows.
s
↔ b(c(c(x658))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(b(c(x659))) ↔ b(c(b(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ b(c(b(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ c(c(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ c(b(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ c(a(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ b(c(c(x659))) ↔ b(c(b(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ b(c(c(x659))) ↔ c(c(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ b(c(c(x659))) ↔ c(b(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ b(c(c(x659))) ↔ c(a(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(a(c(x659))) ↔ b(c(b(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ b(a(c(x659))) ↔ b(c(b(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ c(c(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ c(c(c(x659))) ↔ c(c(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ c(c(c(x659))) ↔ c(b(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ c(c(c(x659))) ↔ c(a(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(a(c(x659))) ↔ c(c(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(a(c(x659))) ↔ c(c(c(x659))) ↔ c(c(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(a(c(x659))) ↔ c(c(c(x659))) ↔ c(b(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(a(c(x659))) ↔ c(c(c(x659))) ↔ c(a(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ a(c(c(x659))) ↔ c(c(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ a(c(c(x659))) ↔ a(c(b(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(c(c(x659))) ↔ a(c(c(x659))) ↔ c(b(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(a(c(x659))) ↔ c(b(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(a(c(x659))) ↔ c(b(c(x659))) ↔ c(c(c(x659))) ↔
t
-
The critical peak s = b(b(c(x659)))←→ε c(c(b(x659))) = t can be joined as follows.
s
↔ b(a(c(x659))) ↔ c(b(c(x659))) ↔ c(b(c(x659))) ↔
t
-
The critical peak s = b(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔ b(c(x)) ↔
t
-
The critical peak s = b(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = b(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = c(b(c(x661)))←→ε a(c(b(x661))) = t can be joined as follows.
s
↔ a(c(c(x661))) ↔
t
-
The critical peak s = c(b(c(x662)))←→ε c(c(b(x662))) = t can be joined as follows.
s
↔ c(b(c(x662))) ↔
t
-
The critical peak s = c(b(c(x662)))←→ε c(c(b(x662))) = t can be joined as follows.
s
↔ c(c(c(x662))) ↔
t
-
The critical peak s = c(b(c(x662)))←→ε c(c(b(x662))) = t can be joined as follows.
s
↔ c(a(c(x662))) ↔
t
-
The critical peak s = b(b(c(x663)))←→ε b(c(b(x663))) = t can be joined as follows.
s
↔ b(b(c(x663))) ↔
t
-
The critical peak s = b(b(c(x663)))←→ε b(c(b(x663))) = t can be joined as follows.
s
↔ b(c(c(x663))) ↔
t
-
The critical peak s = b(b(c(x663)))←→ε b(c(b(x663))) = t can be joined as follows.
s
↔ b(a(c(x663))) ↔
t
-
The critical peak s = b(b(c(x664)))←→ε a(c(b(x664))) = t can be joined as follows.
s
↔ b(a(c(x664))) ↔ a(b(c(x664))) ↔
t
-
The critical peak s = b(b(c(x664)))←→ε a(c(b(x664))) = t can be joined as follows.
s
↔ b(c(c(x664))) ↔ b(a(c(x664))) ↔ a(b(c(x664))) ↔
t
-
The critical peak s = b(b(c(x664)))←→ε a(c(b(x664))) = t can be joined as follows.
s
↔ b(c(c(x664))) ↔ a(c(c(x664))) ↔
t
-
The critical peak s = b(b(c(x664)))←→ε a(c(b(x664))) = t can be joined as follows.
s
↔ b(c(c(x664))) ↔ a(c(c(x664))) ↔ a(c(c(x664))) ↔
t
-
The critical peak s = b(b(c(x664)))←→ε a(c(b(x664))) = t can be joined as follows.
s
↔ b(c(c(x664))) ↔ a(c(c(x664))) ↔ a(b(c(x664))) ↔
t
-
The critical peak s = b(b(c(x664)))←→ε a(c(b(x664))) = t can be joined as follows.
s
↔ b(a(c(x664))) ↔ c(b(c(x664))) ↔ a(b(c(x664))) ↔
t
-
The critical peak s = b(c(x))←→ε a(c(x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = c(a(c(x666)))←→ε b(c(b(x666))) = t can be joined as follows.
s
↔ b(c(c(x666))) ↔
t
-
The critical peak s = b(a(c(x667)))←→ε c(c(b(x667))) = t can be joined as follows.
s
↔ c(b(c(x667))) ↔
t
-
The critical peak s = b(a(c(x667)))←→ε c(c(b(x667))) = t can be joined as follows.
s
↔ c(c(c(x667))) ↔
t
-
The critical peak s = a(c(x))←→ε c(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
-
The critical peak s = c(a(c(x669)))←→ε a(c(b(x669))) = t can be joined as follows.
s
↔ b(c(c(x669))) ↔ b(a(c(x669))) ↔ a(b(c(x669))) ↔
t
-
The critical peak s = c(a(c(x669)))←→ε a(c(b(x669))) = t can be joined as follows.
s
↔ b(c(c(x669))) ↔ a(c(c(x669))) ↔
t
-
The critical peak s = c(a(c(x669)))←→ε a(c(b(x669))) = t can be joined as follows.
s
↔ b(c(c(x669))) ↔ a(c(c(x669))) ↔ a(c(c(x669))) ↔
t
-
The critical peak s = c(a(c(x669)))←→ε a(c(b(x669))) = t can be joined as follows.
s
↔ b(c(c(x669))) ↔ a(c(c(x669))) ↔ a(b(c(x669))) ↔
t
-
The critical peak s = c(a(c(x669)))←→ε a(c(b(x669))) = t can be joined as follows.
s
↔ c(c(c(x669))) ↔ a(c(c(x669))) ↔
t
-
The critical peak s = c(a(c(x669)))←→ε a(c(b(x669))) = t can be joined as follows.
s
↔ c(c(c(x669))) ↔ a(c(c(x669))) ↔ a(c(c(x669))) ↔
t
-
The critical peak s = c(a(c(x669)))←→ε a(c(b(x669))) = t can be joined as follows.
s
↔ c(c(c(x669))) ↔ a(c(c(x669))) ↔ a(b(c(x669))) ↔
t
-
The critical peak s = c(a(c(x669)))←→ε a(c(b(x669))) = t can be joined as follows.
s
↔ c(c(c(x669))) ↔ c(b(c(x669))) ↔ a(b(c(x669))) ↔
t
-
The critical peak s = c(a(c(x670)))←→ε c(c(b(x670))) = t can be joined as follows.
s
↔ c(a(c(x670))) ↔
t
-
The critical peak s = c(a(c(x670)))←→ε c(c(b(x670))) = t can be joined as follows.
s
↔ c(c(c(x670))) ↔
t
-
The critical peak s = b(a(c(x671)))←→ε b(c(b(x671))) = t can be joined as follows.
s
↔ b(a(c(x671))) ↔
t
-
The critical peak s = b(a(c(x672)))←→ε a(c(b(x672))) = t can be joined as follows.
s
↔ b(a(c(x672))) ↔ a(b(c(x672))) ↔
t
-
The critical peak s = b(a(c(x672)))←→ε a(c(b(x672))) = t can be joined as follows.
s
↔ c(b(c(x672))) ↔ a(b(c(x672))) ↔
t
-
The critical peak s = b(a(c(x672)))←→ε a(c(b(x672))) = t can be joined as follows.
s
↔ c(b(c(x672))) ↔ c(b(c(x672))) ↔ a(b(c(x672))) ↔
t
-
The critical peak s = b(a(c(x672)))←→ε a(c(b(x672))) = t can be joined as follows.
s
↔ c(c(c(x672))) ↔ c(b(c(x672))) ↔ a(b(c(x672))) ↔
t
-
The critical peak s = b(a(c(x672)))←→ε a(c(b(x672))) = t can be joined as follows.
s
↔ c(b(c(x672))) ↔ a(c(c(x672))) ↔
t
-
The critical peak s = b(a(c(x672)))←→ε a(c(b(x672))) = t can be joined as follows.
s
↔ c(b(c(x672))) ↔ a(c(c(x672))) ↔ a(c(c(x672))) ↔
t
-
The critical peak s = b(a(c(x672)))←→ε a(c(b(x672))) = t can be joined as follows.
s
↔ c(b(c(x672))) ↔ a(c(c(x672))) ↔ a(b(c(x672))) ↔
t
-
The critical peak s = b(a(c(x672)))←→ε a(c(b(x672))) = t can be joined as follows.
s
↔ c(c(c(x672))) ↔ a(c(c(x672))) ↔
t
-
The critical peak s = b(a(c(x672)))←→ε a(c(b(x672))) = t can be joined as follows.
s
↔ c(c(c(x672))) ↔ a(c(c(x672))) ↔ a(c(c(x672))) ↔
t
-
The critical peak s = b(a(c(x672)))←→ε a(c(b(x672))) = t can be joined as follows.
s
↔ c(c(c(x672))) ↔ a(c(c(x672))) ↔ a(b(c(x672))) ↔
t
-
The critical peak s = a(c(x))←→ε b(c(x)) = t can be joined as follows.
s
↔ a(c(x)) ↔
t
/>