Certification Problem

Input (COPS 1285)

We consider the TRS containing the following rules:

a(b(a(x)))	→	b(a(b(x)))	(1)
b(a(b(x)))	→	a(b(a(x)))	(2)
p	→	a(p)	(3)
p	→	b(p)	(4)

The underlying signature is as follows:

{a/1, b/1, p/0}

Property / Task

Prove or disprove confluence.

Answer / Result

Yes.

Proof (by csi @ CoCo 2022)

1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

p	→	b(p)	(4)
p	→	a(p)	(3)
b(a(b(x)))	→	a(b(a(x)))	(2)
a(b(a(x)))	→	b(a(b(x)))	(1)
p	→	b(b(p))	(5)
p	→	b(a(p))	(6)
p	→	a(b(p))	(7)
p	→	a(a(p))	(8)
b(a(b(x)))	→	b(a(b(x)))	(9)
a(b(a(x)))	→	a(b(a(x)))	(10)

All redundant rules that were added or removed can be simulated in 2 steps .

1.1 Decreasing Diagrams

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

p → b(p) (4)
↦ 2
p → a(p) (3)
↦ 2
b(a(b(x))) → a(b(a(x))) (2)
↦ 0
a(b(a(x))) → b(a(b(x))) (1)
↦ 0
p → b(b(p)) (5)
↦ 8
p → b(a(p)) (6)
↦ 2
p → a(b(p)) (7)
↦ 2
p → a(a(p)) (8)
↦ 8
b(a(b(x))) → b(a(b(x))) (9)
↦ 0
a(b(a(x))) → a(b(a(x))) (10)
↦ 0

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 = b(p)←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(p)←→_ε a(p) = t can be joined as follows.
s ↔ b(a(p)) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(p)←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(p)←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(p)←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(p)) ↔ t
The critical peak s = b(p)←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ t
The critical peak s = b(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ b(b(b(p))) ↔ t
The critical peak s = b(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ b(b(a(p))) ↔ t
The critical peak s = b(p)←→_ε b(a(p)) = t can be joined as follows.
s ↔ t
The critical peak s = b(p)←→_ε b(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ t
The critical peak s = b(p)←→_ε b(a(p)) = t can be joined as follows.
s ↔ b(a(a(p))) ↔ t
The critical peak s = b(p)←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(p)←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(p)) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(p)←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(p)←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(p)) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ t
The critical peak s = b(p)←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ t
The critical peak s = b(p)←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(p)) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(p)←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(p)) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(p)) ↔ b(a(b(p))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(p))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(p)) ↔ b(a(b(b(p)))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(p)))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(p)) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(p)) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ a(a(b(p))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(p)) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(p)) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ a(a(b(p))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ a(a(b(p))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(b(b(p))))) ↔ a(a(b(a(b(p))))) ↔ a(a(b(p))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(b(b(p))))) ↔ a(a(b(a(b(p))))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(b(b(p))))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(b(p))))) ↔ a(b(a(b(b(p))))) ↔ a(a(b(a(b(p))))) ↔ a(a(b(p))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(b(p))))) ↔ a(b(a(b(b(p))))) ↔ a(a(b(a(b(p))))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(b(p))))) ↔ a(b(a(b(b(p))))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(b(a(p))))) ↔ a(a(b(a(a(p))))) ↔ a(a(b(p))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(b(a(p))))) ↔ a(a(b(a(a(p))))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(b(a(p))))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(a(p))))) ↔ a(b(a(b(a(p))))) ↔ a(a(b(a(a(p))))) ↔ a(a(b(p))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(a(p))))) ↔ a(b(a(b(a(p))))) ↔ a(a(b(a(a(p))))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(a(p))))) ↔ a(b(a(b(a(p))))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = a(p)←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(p)←→_ε b(p) = t can be joined as follows.
s ↔ a(b(p)) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(p)←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(p)←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(p)←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(p)) ↔ t
The critical peak s = a(p)←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(p)) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(p)) ↔ a(b(a(p))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(p))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(p)) ↔ a(b(a(a(p)))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(p)))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(p)) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(p)) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ b(b(a(p))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(p)) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(p)) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ b(b(a(p))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ b(b(a(p))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(a(b(p))))) ↔ b(b(a(b(b(p))))) ↔ b(b(a(p))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(a(b(p))))) ↔ b(b(a(b(b(p))))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(a(b(p))))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(b(p))))) ↔ b(a(b(a(b(p))))) ↔ b(b(a(b(b(p))))) ↔ b(b(a(p))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(b(p))))) ↔ b(a(b(a(b(p))))) ↔ b(b(a(b(b(p))))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(b(p))))) ↔ b(a(b(a(b(p))))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(a(a(p))))) ↔ b(b(a(b(a(p))))) ↔ b(b(a(p))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(a(a(p))))) ↔ b(b(a(b(a(p))))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(a(a(p))))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(a(p))))) ↔ b(a(b(a(a(p))))) ↔ b(b(a(b(a(p))))) ↔ b(b(a(p))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(a(p))))) ↔ b(a(b(a(a(p))))) ↔ b(b(a(b(a(p))))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(a(p))))) ↔ b(a(b(a(a(p))))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(p)←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(p)) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(p)←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(p)←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(p)) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ t
The critical peak s = a(p)←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(p)) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ t
The critical peak s = a(p)←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ t
The critical peak s = a(p)←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(p)←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(p)←→_ε a(b(p)) = t can be joined as follows.
s ↔ t
The critical peak s = a(p)←→_ε a(b(p)) = t can be joined as follows.
s ↔ a(b(b(p))) ↔ t
The critical peak s = a(p)←→_ε a(b(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ t
The critical peak s = a(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ t
The critical peak s = a(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ a(a(b(p))) ↔ t
The critical peak s = a(p)←→_ε a(a(p)) = t can be joined as follows.
s ↔ a(a(a(p))) ↔ t
The critical peak s = b(a(a(b(a(x93)))))←→_ε a(b(a(a(b(x93))))) = t can be joined as follows.
s ↔ b(a(b(a(b(x93))))) ↔ t
The critical peak s = a(a(b(a(x94))))←→_ε b(a(b(b(x94)))) = t can be joined as follows.
s ↔ a(b(a(b(x94)))) ↔ t
The critical peak s = a(b(a(x)))←→_ε b(a(b(x))) = t can be joined as follows.
s ↔ a(b(a(x))) ↔ t
The critical peak s = a(b(a(x)))←→_ε b(a(b(x))) = t can be joined as follows.
s ↔ t
The critical peak s = b(a(a(b(a(x96)))))←→_ε b(a(b(a(b(x96))))) = t can be joined as follows.
s ↔ b(a(a(b(a(x96))))) ↔ t
The critical peak s = b(a(a(b(a(x96)))))←→_ε b(a(b(a(b(x96))))) = t can be joined as follows.
s ↔ t
The critical peak s = a(a(b(a(x97))))←→_ε a(b(a(b(x97)))) = t can be joined as follows.
s ↔ a(a(b(a(x97)))) ↔ t
The critical peak s = a(a(b(a(x97))))←→_ε a(b(a(b(x97)))) = t can be joined as follows.
s ↔ t
The critical peak s = b(b(a(b(x98))))←→_ε a(b(a(a(x98)))) = t can be joined as follows.
s ↔ b(a(b(a(x98)))) ↔ t
The critical peak s = a(b(b(a(b(x99)))))←→_ε b(a(b(b(a(x99))))) = t can be joined as follows.
s ↔ a(b(a(b(a(x99))))) ↔ t
The critical peak s = b(b(a(b(x100))))←→_ε b(a(b(a(x100)))) = t can be joined as follows.
s ↔ b(b(a(b(x100)))) ↔ t
The critical peak s = b(b(a(b(x100))))←→_ε b(a(b(a(x100)))) = t can be joined as follows.
s ↔ t
The critical peak s = b(a(b(x)))←→_ε a(b(a(x))) = t can be joined as follows.
s ↔ b(a(b(x))) ↔ t
The critical peak s = b(a(b(x)))←→_ε a(b(a(x))) = t can be joined as follows.
s ↔ t
The critical peak s = a(b(b(a(b(x102)))))←→_ε a(b(a(b(a(x102))))) = t can be joined as follows.
s ↔ a(b(b(a(b(x102))))) ↔ t
The critical peak s = a(b(b(a(b(x102)))))←→_ε a(b(a(b(a(x102))))) = t can be joined as follows.
s ↔ t
The critical peak s = b(b(p))←→_ε b(p) = t can be joined as follows.
s ↔ b(b(p)) ↔ t
The critical peak s = b(b(p))←→_ε b(p) = t can be joined as follows.
s ↔ b(b(b(p))) ↔ t
The critical peak s = b(b(p))←→_ε b(p) = t can be joined as follows.
s ↔ b(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(p)) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(p))) ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(p)) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(p))) ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(p))) ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(p)) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(p)) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(p))) ↔ b(b(a(b(b(p))))) ↔ b(a(b(a(b(p))))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(p))) ↔ b(b(a(b(b(p))))) ↔ b(a(b(a(b(p))))) ↔ a(b(a(a(b(p))))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(b(a(b(b(p))))) ↔ b(a(b(a(b(p))))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(b(a(b(b(p))))) ↔ b(a(b(a(b(p))))) ↔ a(b(a(a(b(p))))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(b(p))))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(b(p))))) ↔ a(b(a(a(b(p))))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(p))) ↔ b(b(a(b(a(p))))) ↔ b(a(b(a(a(p))))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(p))) ↔ b(b(a(b(a(p))))) ↔ b(a(b(a(a(p))))) ↔ a(b(a(a(a(p))))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(b(a(b(a(p))))) ↔ b(a(b(a(a(p))))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(b(a(b(a(p))))) ↔ b(a(b(a(a(p))))) ↔ a(b(a(a(a(p))))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(a(p))))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(a(p))))) ↔ a(b(a(a(a(p))))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(p)) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(p))) ↔ a(b(p)) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(p)) ↔ t
The critical peak s = b(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ b(b(a(p))) ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(p))) ↔ t
The critical peak s = b(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(a(b(a(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(a(b(a(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ a(a(b(a(a(b(p)))))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(b(a(p)))))) ↔ a(b(a(a(b(a(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(b(a(p)))))) ↔ a(b(a(a(b(a(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ a(a(b(a(a(b(p)))))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(b(a(b(b(a(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ a(b(a(a(b(a(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(b(a(b(b(a(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ a(b(a(a(b(a(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ a(a(b(a(a(b(p)))))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(b(a(p)))))) ↔ b(a(b(b(a(b(p)))))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(b(a(p)))))) ↔ b(a(b(b(a(b(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(b(a(p)))))) ↔ b(a(b(b(a(b(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ a(a(b(a(a(b(p)))))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(b(a(b(b(a(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ b(a(b(b(a(b(p)))))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(b(a(b(b(a(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ b(a(b(b(a(b(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(b(a(b(p)))) ↔ b(b(a(b(b(a(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ b(a(b(b(a(b(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ a(a(b(a(a(b(p)))))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = b(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ b(a(p)) ↔ t
The critical peak s = b(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ t
The critical peak s = b(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ b(a(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(p)) ↔ t
The critical peak s = b(a(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(b(p)) ↔ t
The critical peak s = b(a(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(p)) ↔ t
The critical peak s = b(a(p))←→_ε a(p) = t can be joined as follows.
s ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = b(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = b(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ b(a(b(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = b(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = b(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ b(b(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(b(p)))) ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(a(p)))) ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(p))) ↔ a(b(a(p))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(p)))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(p))) ↔ t
The critical peak s = b(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ b(a(b(a(p)))) ↔ a(b(a(a(p)))) ↔ a(b(a(a(p)))) ↔ t
The critical peak s = b(a(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ b(a(b(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = a(b(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(p)) ↔ t
The critical peak s = a(b(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(p)) ↔ t
The critical peak s = a(b(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(a(p)) ↔ t
The critical peak s = a(b(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ a(b(p)) ↔ t
The critical peak s = a(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ a(b(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε a(p) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ t
The critical peak s = a(b(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(b(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(a(p)))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(b(p)))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(a(b(a(p)))) ↔ t
The critical peak s = a(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = a(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ a(b(a(p))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = a(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ a(b(a(b(p)))) ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = a(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = a(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ a(a(b(p))) ↔ t
The critical peak s = a(b(p))←→_ε a(a(p)) = t can be joined as follows.
s ↔ a(b(a(b(p)))) ↔ a(a(b(a(p)))) ↔ a(a(b(a(p)))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(p)) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(p))) ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(p)) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(p))) ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(p))) ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(p)) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(p)) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(p))) ↔ a(a(b(a(b(p))))) ↔ a(b(a(b(b(p))))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(p))) ↔ a(a(b(a(b(p))))) ↔ a(b(a(b(b(p))))) ↔ b(a(b(b(b(p))))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(a(b(a(b(p))))) ↔ a(b(a(b(b(p))))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(a(b(a(b(p))))) ↔ a(b(a(b(b(p))))) ↔ b(a(b(b(b(p))))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(b(p))))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(b(p))))) ↔ b(a(b(b(b(p))))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(p))) ↔ a(a(b(a(a(p))))) ↔ a(b(a(b(a(p))))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(p))) ↔ a(a(b(a(a(p))))) ↔ a(b(a(b(a(p))))) ↔ b(a(b(b(a(p))))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(a(b(a(a(p))))) ↔ a(b(a(b(a(p))))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(a(b(a(a(p))))) ↔ a(b(a(b(a(p))))) ↔ b(a(b(b(a(p))))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(a(p))))) ↔ a(b(a(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(a(p))))) ↔ b(a(b(b(a(p))))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(p)) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(p))) ↔ b(a(p)) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(p))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(p)) ↔ t
The critical peak s = a(a(p))←→_ε b(p) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε a(p) = t can be joined as follows.
s ↔ a(a(p)) ↔ t
The critical peak s = a(a(p))←→_ε a(p) = t can be joined as follows.
s ↔ a(a(b(p))) ↔ t
The critical peak s = a(a(p))←→_ε a(p) = t can be joined as follows.
s ↔ a(a(a(p))) ↔ t
The critical peak s = a(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(b(a(b(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ b(a(b(b(a(b(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ b(b(a(b(b(a(p)))))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(a(b(p)))))) ↔ b(a(b(b(a(b(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(a(b(p)))))) ↔ b(a(b(b(a(b(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ b(b(a(b(b(a(p)))))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(a(b(a(a(b(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ b(a(b(b(a(b(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(a(b(a(a(b(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ b(a(b(b(a(b(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ b(b(a(b(b(a(p)))))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(a(b(p)))))) ↔ a(b(a(a(b(a(p)))))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(a(b(p)))))) ↔ a(b(a(a(b(a(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(a(b(p)))))) ↔ a(b(a(a(b(a(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ b(b(a(b(b(a(p)))))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(a(b(a(a(b(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ a(b(a(a(b(a(p)))))) ↔ a(b(a(a(p)))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(a(b(a(a(b(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ a(b(a(a(b(a(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ b(a(b(a(p)))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε b(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(a(b(a(a(b(p)))))) ↔ a(b(a(b(a(b(p)))))) ↔ a(b(a(a(b(a(p)))))) ↔ b(a(b(a(b(a(p)))))) ↔ b(b(a(b(b(a(p)))))) ↔ b(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε b(a(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ b(a(b(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ a(a(b(p))) ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ t
The critical peak s = a(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(p))) ↔ t
The critical peak s = a(a(p))←→_ε a(b(p)) = t can be joined as follows.
s ↔ a(a(b(a(p)))) ↔ a(b(a(b(p)))) ↔ a(b(a(b(p)))) ↔ t
The critical peak s = b(a(b(x)))←→_ε a(b(a(x))) = t can be joined as follows.
s ↔ b(a(b(x))) ↔ t
The critical peak s = b(a(b(x)))←→_ε a(b(a(x))) = t can be joined as follows.
s ↔ t
The critical peak s = b(a(b(a(b(x104)))))←→_ε a(b(a(a(b(x104))))) = t can be joined as follows.
s ↔ b(a(b(a(b(x104))))) ↔ t
The critical peak s = b(a(b(a(b(x104)))))←→_ε a(b(a(a(b(x104))))) = t can be joined as follows.
s ↔ t
The critical peak s = a(b(a(b(x105))))←→_ε b(a(b(b(x105)))) = t can be joined as follows.
s ↔ a(b(a(b(x105)))) ↔ t
The critical peak s = a(b(a(b(x105))))←→_ε b(a(b(b(x105)))) = t can be joined as follows.
s ↔ t
The critical peak s = b(a(b(a(b(x106)))))←→_ε b(a(b(a(b(x106))))) = t can be joined as follows.
s ↔ t
The critical peak s = a(b(a(b(x107))))←→_ε a(b(a(b(x107)))) = t can be joined as follows.
s ↔ t
The critical peak s = b(a(b(a(x108))))←→_ε a(b(a(a(x108)))) = t can be joined as follows.
s ↔ b(a(b(a(x108)))) ↔ t
The critical peak s = b(a(b(a(x108))))←→_ε a(b(a(a(x108)))) = t can be joined as follows.
s ↔ t
The critical peak s = a(b(a(x)))←→_ε b(a(b(x))) = t can be joined as follows.
s ↔ a(b(a(x))) ↔ t
The critical peak s = a(b(a(x)))←→_ε b(a(b(x))) = t can be joined as follows.
s ↔ t
The critical peak s = a(b(a(b(a(x110)))))←→_ε b(a(b(b(a(x110))))) = t can be joined as follows.
s ↔ a(b(a(b(a(x110))))) ↔ t
The critical peak s = a(b(a(b(a(x110)))))←→_ε b(a(b(b(a(x110))))) = t can be joined as follows.
s ↔ t
The critical peak s = b(a(b(a(x111))))←→_ε b(a(b(a(x111)))) = t can be joined as follows.
s ↔ t
The critical peak s = a(b(a(b(a(x112)))))←→_ε a(b(a(b(a(x112))))) = t can be joined as follows.
s ↔ t