Certification Problem
Input (COPS 60)
We consider the TRS containing the following rules:
|
+(x,+(y,z)) |
→ |
+(+(x,y),z) |
(1) |
|
+(+(x,y),z) |
→ |
+(x,+(y,z)) |
(2) |
|
+(x,y) |
→ |
+(y,x) |
(3) |
|
+(s(x),y) |
→ |
+(x,s(y)) |
(4) |
|
+(x,s(y)) |
→ |
+(s(x),y) |
(5) |
|
*(x,s(y)) |
→ |
+(x,*(x,y)) |
(6) |
|
*(s(x),y) |
→ |
+(*(x,y),y) |
(7) |
|
*(x,y) |
→ |
*(y,x) |
(8) |
|
sq(x) |
→ |
*(x,x) |
(9) |
|
sq(s(x)) |
→ |
+(*(x,x),s(+(x,x))) |
(10) |
The underlying signature is as follows:
{+/2, s/1, */2, sq/1}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by csi @ CoCo 2022)
1 Decreasing Diagrams
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).
-
|
+(x,+(y,z)) |
→ |
+(+(x,y),z) |
(1) |
↦ 0
-
|
+(+(x,y),z) |
→ |
+(x,+(y,z)) |
(2) |
↦ 0
-
↦ 0
-
|
+(s(x),y) |
→ |
+(x,s(y)) |
(4) |
↦ 0
-
|
+(x,s(y)) |
→ |
+(s(x),y) |
(5) |
↦ 0
-
|
*(x,s(y)) |
→ |
+(x,*(x,y)) |
(6) |
↦ 1
-
|
*(s(x),y) |
→ |
+(*(x,y),y) |
(7) |
↦ 1
-
↦ 0
-
↦ 10
-
|
sq(s(x)) |
→ |
+(*(x,x),s(+(x,x))) |
(10) |
↦ 4
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 = +(x,+(+(y,x344),x345))←→ε +(+(x,y),+(x344,x345)) = t can be joined as follows.
s
↔ +(x,+(y,+(x344,x345))) ↔
t
-
The critical peak s = +(+(+(x,y),x347),x348)←→ε +(x,+(y,+(x347,x348))) = t can be joined as follows.
s
↔ +(+(x,y),+(x347,x348)) ↔
t
-
The critical peak s = +(+(+(x,x350),x351),z)←→ε +(x,+(+(x350,x351),z)) = t can be joined as follows.
s
↔ +(+(x,+(x350,x351)),z) ↔
t
-
The critical peak s = +(+(x,x353),x354)←→ε +(+(x353,x354),x) = t can be joined as follows.
s
↔ +(x,+(x353,x354)) ↔
t
-
The critical peak s = +(+(s(x),x356),x357)←→ε +(x,s(+(x356,x357))) = t can be joined as follows.
s
↔ +(s(x),+(x356,x357)) ↔
t
-
The critical peak s = +(x358,+(x359,+(y,z)))←→ε +(+(+(x358,x359),y),z) = t can be joined as follows.
s
↔ +(+(x358,x359),+(y,z)) ↔
t
-
The critical peak s = +(x,+(x361,+(x362,z)))←→ε +(+(x,+(x361,x362)),z) = t can be joined as follows.
s
↔ +(x,+(+(x361,x362),z)) ↔
t
-
The critical peak s = +(+(x364,+(x365,y)),z)←→ε +(+(x364,x365),+(y,z)) = t can be joined as follows.
s
↔ +(+(+(x364,x365),y),z) ↔
t
-
The critical peak s = +(x367,+(x368,y))←→ε +(y,+(x367,x368)) = t can be joined as follows.
s
↔ +(+(x367,x368),y) ↔
t
-
The critical peak s = +(x370,+(x371,s(y)))←→ε +(s(+(x370,x371)),y) = t can be joined as follows.
s
↔ +(+(x370,x371),s(y)) ↔
t
-
The critical peak s = +(+(y,z),x)←→ε +(+(x,y),z) = t can be joined as follows.
s
↔ +(x,+(y,z)) ↔
t
-
The critical peak s = +(x,+(z,y))←→ε +(+(x,y),z) = t can be joined as follows.
s
↔ +(x,+(y,z)) ↔
t
-
The critical peak s = +(z,+(x,y))←→ε +(x,+(y,z)) = t can be joined as follows.
s
↔ +(+(x,y),z) ↔
t
-
The critical peak s = +(+(y,x),z)←→ε +(x,+(y,z)) = t can be joined as follows.
s
↔ +(+(x,y),z) ↔
t
-
The critical peak s = +(y,s(x))←→ε +(x,s(y)) = t can be joined as follows.
s
↔ +(s(x),y) ↔
t
-
The critical peak s = +(y,s(x))←→ε +(x,s(y)) = t can be joined as follows.
s
↔ +(s(y),x) ↔
t
-
The critical peak s = +(s(y),x)←→ε +(s(x),y) = t can be joined as follows.
s
↔ +(x,s(y)) ↔
t
-
The critical peak s = +(s(y),x)←→ε +(s(x),y) = t can be joined as follows.
s
↔ +(y,s(x)) ↔
t
-
The critical peak s = +(x385,s(+(y,z)))←→ε +(+(s(x385),y),z) = t can be joined as follows.
s
↔ +(s(x385),+(y,z)) ↔
t
-
The critical peak s = +(x,+(x387,s(z)))←→ε +(+(x,s(x387)),z) = t can be joined as follows.
s
↔ +(x,+(s(x387),z)) ↔
t
-
The critical peak s = +(+(x389,s(y)),z)←→ε +(s(x389),+(y,z)) = t can be joined as follows.
s
↔ +(+(s(x389),y),z) ↔
t
-
The critical peak s = +(x391,s(y))←→ε +(y,s(x391)) = t can be joined as follows.
s
↔ +(s(y),x391) ↔
t
-
The critical peak s = +(x391,s(y))←→ε +(y,s(x391)) = t can be joined as follows.
s
↔ +(s(x391),y) ↔
t
-
The critical peak s = +(x393,s(s(y)))←→ε +(s(s(x393)),y) = t can be joined as follows.
s
↔ +(s(x393),s(y)) ↔
t
-
The critical peak s = +(x,+(s(y),x396))←→ε +(+(x,y),s(x396)) = t can be joined as follows.
s
↔ +(x,+(y,s(x396))) ↔
t
-
The critical peak s = +(s(+(x,y)),x398)←→ε +(x,+(y,s(x398))) = t can be joined as follows.
s
↔ +(+(x,y),s(x398)) ↔
t
-
The critical peak s = +(+(s(x),x400),z)←→ε +(x,+(s(x400),z)) = t can be joined as follows.
s
↔ +(+(x,s(x400)),z) ↔
t
-
The critical peak s = +(s(x),x402)←→ε +(s(x402),x) = t can be joined as follows.
s
↔ +(x402,s(x)) ↔
t
-
The critical peak s = +(s(x),x402)←→ε +(s(x402),x) = t can be joined as follows.
s
↔ +(x,s(x402)) ↔
t
-
The critical peak s = +(s(s(x)),x404)←→ε +(x,s(s(x404))) = t can be joined as follows.
s
↔ +(s(x),s(x404)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(+(s(x),*(x,x406)),x406) ↔ +(+(x,s(*(x,x406))),x406) ↔ +(x,+(s(*(x,x406)),x406)) ↔ +(x,+(*(x,x406),s(x406))) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(*(s(x),x406),s(x)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(*(x,x406),+(s(x),x406)) ↔ +(*(x,x406),+(x,s(x406))) ↔ +(+(*(x,x406),x),s(x406)) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(*(x,x406),+(s(x),x406)) ↔ +(*(x,x406),+(x,s(x406))) ↔ +(+(*(x,x406),x),s(x406)) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(+(s(x),*(x,x406)),x406) ↔ +(+(*(x,x406),s(x)),x406) ↔ +(*(x,x406),+(s(x),x406)) ↔ +(*(x,x406),+(x,s(x406))) ↔ +(+(*(x,x406),x),s(x406)) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(s(x),+(x406,*(x,x406))) ↔ +(+(s(x),x406),*(x,x406)) ↔ +(*(x,x406),+(s(x),x406)) ↔ +(*(x,x406),+(x,s(x406))) ↔ +(+(*(x,x406),x),s(x406)) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(*(s(x),x406),s(x)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(+(x406,s(x)),*(x,x406)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(s(x406),*(x,s(x406))) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(*(s(x),x406),s(x)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(+(x406,s(x)),*(x,x406)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(+(x406,s(x)),*(x,x406)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(s(x406),*(x,s(x406))) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(+(x406,s(x)),*(x,x406)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(+(s(x),*(x,x406)),x406) ↔ +(x406,+(s(x),*(x,x406))) ↔ +(+(x406,s(x)),*(x,x406)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(s(x406),*(x,s(x406))) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(+(s(x),*(x,x406)),x406) ↔ +(x406,+(s(x),*(x,x406))) ↔ +(+(x406,s(x)),*(x,x406)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(s(x),+(x406,*(x,x406))) ↔ +(+(s(x),x406),*(x,x406)) ↔ +(+(x406,s(x)),*(x,x406)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(s(x406),*(x,s(x406))) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(s(x),+(x406,*(x,x406))) ↔ +(+(s(x),x406),*(x,x406)) ↔ +(+(x406,s(x)),*(x,x406)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(*(s(x),x406),s(x)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(*(x,x406),+(s(x406),x)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(s(x406),*(x,s(x406))) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(*(s(x),x406),s(x)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(*(x,x406),+(s(x406),x)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(*(s(x),x406),s(x)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(*(x,x406),+(s(x406),x)) ↔ +(+(*(x,x406),s(x406)),x) ↔ +(x,+(*(x,x406),s(x406))) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(*(s(x),x406),s(x)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(*(x,x406),+(s(x406),x)) ↔ +(*(x,x406),+(x,s(x406))) ↔ +(+(*(x,x406),x),s(x406)) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(*(x,x406),+(s(x406),x)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(s(x406),*(x,s(x406))) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(*(x,x406),+(s(x406),x)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(*(x,x406),+(s(x406),x)) ↔ +(+(*(x,x406),s(x406)),x) ↔ +(x,+(*(x,x406),s(x406))) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(+(*(x,x406),x406),s(x)) ↔ +(*(x,x406),+(x406,s(x))) ↔ +(*(x,x406),+(s(x406),x)) ↔ +(*(x,x406),+(x,s(x406))) ↔ +(+(*(x,x406),x),s(x406)) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(+(s(x),*(x,x406)),x406) ↔ +(+(x,s(*(x,x406))),x406) ↔ +(x,+(s(*(x,x406)),x406)) ↔ +(x,+(*(x,x406),s(x406))) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(s(x),+(x406,*(x,x406))) ↔ +(+(s(x),x406),*(x,x406)) ↔ +(+(x,s(x406)),*(x,x406)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(s(x406),*(x,s(x406))) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(s(x),+(x406,*(x,x406))) ↔ +(+(s(x),x406),*(x,x406)) ↔ +(+(x,s(x406)),*(x,x406)) ↔ +(+(s(x406),x),*(x,x406)) ↔ +(s(x406),+(x,*(x,x406))) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(s(x),+(x406,*(x,x406))) ↔ +(+(s(x),x406),*(x,x406)) ↔ +(+(x,s(x406)),*(x,x406)) ↔ +(x,+(s(x406),*(x,x406))) ↔ +(x,+(*(x,x406),s(x406))) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),+(*(x,x406),x406)) ↔ +(s(x),+(x406,*(x,x406))) ↔ +(+(s(x),x406),*(x,x406)) ↔ +(+(x,s(x406)),*(x,x406)) ↔ +(*(x,x406),+(x,s(x406))) ↔ +(+(*(x,x406),x),s(x406)) ↔ +(+(x,*(x,x406)),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),*(x406,s(x))) ↔ +(s(x),+(x406,*(x406,x))) ↔ +(+(s(x),x406),*(x406,x)) ↔ +(*(x406,x),+(s(x),x406)) ↔ +(*(x406,x),+(x,s(x406))) ↔ +(+(*(x406,x),x),s(x406)) ↔ +(*(s(x406),x),s(x406)) ↔
t
-
The critical peak s = +(s(x),*(s(x),x406))←→ε +(*(x,s(x406)),s(x406)) = t can be joined as follows.
s
↔ +(s(x),*(x406,s(x))) ↔ +(s(x),+(x406,*(x406,x))) ↔ +(+(s(x),x406),*(x406,x)) ↔ +(+(x,s(x406)),*(x406,x)) ↔ +(*(x406,x),+(x,s(x406))) ↔ +(+(*(x406,x),x),s(x406)) ↔ +(*(s(x406),x),s(x406)) ↔
t
-
The critical peak s = +(x,*(x,x408))←→ε *(s(x408),x) = t can be joined as follows.
s
↔ +(x,*(x,x408)) ↔ *(x,s(x408)) ↔
t
-
The critical peak s = +(x,*(x,x408))←→ε *(s(x408),x) = t can be joined as follows.
s
↔ +(*(x,x408),x) ↔ +(*(x408,x),x) ↔
t
-
The critical peak s = +(x,*(x,x408))←→ε *(s(x408),x) = t can be joined as follows.
s
↔ +(x,*(x408,x)) ↔ +(*(x408,x),x) ↔
t
-
The critical peak s = +(x,*(x,x408))←→ε *(s(x408),x) = t can be joined as follows.
s
↔ +(*(x,x408),x) ↔ +(*(x408,x),x) ↔
t
-
The critical peak s = +(x,*(x,x408))←→ε *(s(x408),x) = t can be joined as follows.
s
↔ +(x,*(x408,x)) ↔ +(*(x408,x),x) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(x409,+(*(x409,y),s(y))) ↔ +(x409,+(s(*(x409,y)),y)) ↔ +(+(x409,s(*(x409,y))),y) ↔ +(+(s(x409),*(x409,y)),y) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(s(y),*(x409,s(y))) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(+(x409,s(y)),*(x409,y)) ↔ +(+(s(x409),y),*(x409,y)) ↔ +(s(x409),+(y,*(x409,y))) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(+(x409,s(y)),*(x409,y)) ↔ +(+(s(x409),y),*(x409,y)) ↔ +(s(x409),+(y,*(x409,y))) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(x409,+(*(x409,y),s(y))) ↔ +(x409,+(s(y),*(x409,y))) ↔ +(+(x409,s(y)),*(x409,y)) ↔ +(+(s(x409),y),*(x409,y)) ↔ +(s(x409),+(y,*(x409,y))) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(+(*(x409,y),x409),s(y)) ↔ +(*(x409,y),+(x409,s(y))) ↔ +(+(x409,s(y)),*(x409,y)) ↔ +(+(s(x409),y),*(x409,y)) ↔ +(s(x409),+(y,*(x409,y))) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(s(y),*(x409,s(y))) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(*(x409,y),+(s(y),x409)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(*(s(x409),y),s(x409)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(s(y),*(x409,s(y))) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(*(x409,y),+(s(y),x409)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(*(x409,y),+(s(y),x409)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(*(s(x409),y),s(x409)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(*(x409,y),+(s(y),x409)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(x409,+(*(x409,y),s(y))) ↔ +(+(*(x409,y),s(y)),x409) ↔ +(*(x409,y),+(s(y),x409)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(*(s(x409),y),s(x409)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(x409,+(*(x409,y),s(y))) ↔ +(+(*(x409,y),s(y)),x409) ↔ +(*(x409,y),+(s(y),x409)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(+(*(x409,y),x409),s(y)) ↔ +(*(x409,y),+(x409,s(y))) ↔ +(*(x409,y),+(s(y),x409)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(*(s(x409),y),s(x409)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(+(*(x409,y),x409),s(y)) ↔ +(*(x409,y),+(x409,s(y))) ↔ +(*(x409,y),+(s(y),x409)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(s(y),*(x409,s(y))) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(+(y,s(x409)),*(x409,y)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(*(s(x409),y),s(x409)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(s(y),*(x409,s(y))) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(+(y,s(x409)),*(x409,y)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(s(y),*(x409,s(y))) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(+(y,s(x409)),*(x409,y)) ↔ +(y,+(s(x409),*(x409,y))) ↔ +(+(s(x409),*(x409,y)),y) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(s(y),*(x409,s(y))) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(+(y,s(x409)),*(x409,y)) ↔ +(+(s(x409),y),*(x409,y)) ↔ +(s(x409),+(y,*(x409,y))) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(+(y,s(x409)),*(x409,y)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(*(s(x409),y),s(x409)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(+(y,s(x409)),*(x409,y)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(+(y,s(x409)),*(x409,y)) ↔ +(y,+(s(x409),*(x409,y))) ↔ +(+(s(x409),*(x409,y)),y) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(s(y),+(x409,*(x409,y))) ↔ +(+(s(y),x409),*(x409,y)) ↔ +(+(y,s(x409)),*(x409,y)) ↔ +(+(s(x409),y),*(x409,y)) ↔ +(s(x409),+(y,*(x409,y))) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(x409,+(*(x409,y),s(y))) ↔ +(x409,+(s(*(x409,y)),y)) ↔ +(+(x409,s(*(x409,y))),y) ↔ +(+(s(x409),*(x409,y)),y) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(+(*(x409,y),x409),s(y)) ↔ +(*(x409,y),+(x409,s(y))) ↔ +(*(x409,y),+(s(x409),y)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(*(s(x409),y),s(x409)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(+(*(x409,y),x409),s(y)) ↔ +(*(x409,y),+(x409,s(y))) ↔ +(*(x409,y),+(s(x409),y)) ↔ +(*(x409,y),+(y,s(x409))) ↔ +(+(*(x409,y),y),s(x409)) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(+(*(x409,y),x409),s(y)) ↔ +(*(x409,y),+(x409,s(y))) ↔ +(*(x409,y),+(s(x409),y)) ↔ +(+(*(x409,y),s(x409)),y) ↔ +(+(s(x409),*(x409,y)),y) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(+(x409,*(x409,y)),s(y)) ↔ +(+(*(x409,y),x409),s(y)) ↔ +(*(x409,y),+(x409,s(y))) ↔ +(*(x409,y),+(s(x409),y)) ↔ +(+(s(x409),y),*(x409,y)) ↔ +(s(x409),+(y,*(x409,y))) ↔ +(s(x409),+(*(x409,y),y)) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(*(s(y),x409),s(y)) ↔ +(+(*(y,x409),x409),s(y)) ↔ +(*(y,x409),+(x409,s(y))) ↔ +(+(x409,s(y)),*(y,x409)) ↔ +(+(s(x409),y),*(y,x409)) ↔ +(s(x409),+(y,*(y,x409))) ↔ +(s(x409),*(y,s(x409))) ↔
t
-
The critical peak s = +(*(x409,s(y)),s(y))←→ε +(s(x409),*(s(x409),y)) = t can be joined as follows.
s
↔ +(*(s(y),x409),s(y)) ↔ +(+(*(y,x409),x409),s(y)) ↔ +(*(y,x409),+(x409,s(y))) ↔ +(*(y,x409),+(s(x409),y)) ↔ +(+(s(x409),y),*(y,x409)) ↔ +(s(x409),+(y,*(y,x409))) ↔ +(s(x409),*(y,s(x409))) ↔
t
-
The critical peak s = +(*(x411,y),y)←→ε *(y,s(x411)) = t can be joined as follows.
s
↔ +(*(x411,y),y) ↔ *(s(x411),y) ↔
t
-
The critical peak s = +(*(x411,y),y)←→ε *(y,s(x411)) = t can be joined as follows.
s
↔ +(y,*(x411,y)) ↔ +(y,*(y,x411)) ↔
t
-
The critical peak s = +(*(x411,y),y)←→ε *(y,s(x411)) = t can be joined as follows.
s
↔ +(*(y,x411),y) ↔ +(y,*(y,x411)) ↔
t
-
The critical peak s = +(*(x411,y),y)←→ε *(y,s(x411)) = t can be joined as follows.
s
↔ +(y,*(x411,y)) ↔ +(y,*(y,x411)) ↔
t
-
The critical peak s = +(*(x411,y),y)←→ε *(y,s(x411)) = t can be joined as follows.
s
↔ +(*(y,x411),y) ↔ +(y,*(y,x411)) ↔
t
-
The critical peak s = *(s(y),x)←→ε +(x,*(x,y)) = t can be joined as follows.
s
↔ +(*(y,x),x) ↔ +(*(x,y),x) ↔
t
-
The critical peak s = *(s(y),x)←→ε +(x,*(x,y)) = t can be joined as follows.
s
↔ +(*(y,x),x) ↔ +(x,*(y,x)) ↔
t
-
The critical peak s = *(s(y),x)←→ε +(x,*(x,y)) = t can be joined as follows.
s
↔ +(*(y,x),x) ↔ +(x,*(y,x)) ↔
t
-
The critical peak s = *(s(y),x)←→ε +(x,*(x,y)) = t can be joined as follows.
s
↔ +(*(y,x),x) ↔ +(*(x,y),x) ↔
t
-
The critical peak s = *(s(y),x)←→ε +(x,*(x,y)) = t can be joined as follows.
s
↔ *(x,s(y)) ↔
t
-
The critical peak s = *(y,s(x))←→ε +(*(x,y),y) = t can be joined as follows.
s
↔ +(y,*(y,x)) ↔ +(y,*(x,y)) ↔
t
-
The critical peak s = *(y,s(x))←→ε +(*(x,y),y) = t can be joined as follows.
s
↔ +(y,*(y,x)) ↔ +(*(y,x),y) ↔
t
-
The critical peak s = *(y,s(x))←→ε +(*(x,y),y) = t can be joined as follows.
s
↔ +(y,*(y,x)) ↔ +(*(y,x),y) ↔
t
-
The critical peak s = *(y,s(x))←→ε +(*(x,y),y) = t can be joined as follows.
s
↔ +(y,*(y,x)) ↔ +(y,*(x,y)) ↔
t
-
The critical peak s = *(y,s(x))←→ε +(*(x,y),y) = t can be joined as follows.
s
↔ *(s(x),y) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(x,s(*(x,x))),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(x,s(*(x,x))),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(x,s(*(x,x))),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(s(*(x,x)),x)) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(s(*(x,x)),x)) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(s(*(x,x)),x)) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(*(x,x),s(x))) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(*(x,x),s(x)),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(x,+(s(x),*(x,x))) ↔ +(x,+(x,s(*(x,x)))) ↔ +(+(x,x),s(*(x,x))) ↔ +(s(+(x,x)),*(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(x,+(s(x),*(x,x))) ↔ +(x,+(x,s(*(x,x)))) ↔ +(+(x,x),s(*(x,x))) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(s(x),*(x,x))) ↔ +(x,+(x,s(*(x,x)))) ↔ +(+(x,x),s(*(x,x))) ↔ +(s(+(x,x)),*(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(s(x),*(x,x))) ↔ +(x,+(x,s(*(x,x)))) ↔ +(+(x,x),s(*(x,x))) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(x,s(*(x,x))),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(x,s(*(x,x))),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(x,s(*(x,x))),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(x,s(*(x,x))),x) ↔ +(x,+(x,s(*(x,x)))) ↔ +(+(x,x),s(*(x,x))) ↔ +(s(+(x,x)),*(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(x,s(*(x,x))),x) ↔ +(x,+(x,s(*(x,x)))) ↔ +(+(x,x),s(*(x,x))) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(x,s(*(x,x))),x) ↔ +(+(x,s(*(x,x))),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(s(x),*(s(x),x)) ↔ +(s(x),+(*(x,x),x)) ↔ +(+(s(x),*(x,x)),x) ↔ +(+(x,s(*(x,x))),x) ↔ +(x,+(s(*(x,x)),x)) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(s(*(x,x)),x)) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(s(*(x,x)),x)) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(s(*(x,x)),x)) ↔ +(+(s(*(x,x)),x),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(s(*(x,x)),x)) ↔ +(x,+(x,s(*(x,x)))) ↔ +(+(x,x),s(*(x,x))) ↔ +(s(+(x,x)),*(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(s(*(x,x)),x)) ↔ +(x,+(x,s(*(x,x)))) ↔ +(+(x,x),s(*(x,x))) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(s(*(x,x)),x)) ↔ +(+(x,s(*(x,x))),x) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = *(s(x),s(x))←→ε +(*(x,x),s(+(x,x))) = t can be joined as follows.
s
↔ +(*(x,s(x)),s(x)) ↔ +(+(x,*(x,x)),s(x)) ↔ +(x,+(*(x,x),s(x))) ↔ +(x,+(s(*(x,x)),x)) ↔ +(x,+(s(*(x,x)),x)) ↔ +(+(s(*(x,x)),x),x) ↔ +(s(*(x,x)),+(x,x)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(x418,s(*(x418,x418))),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(x418,s(*(x418,x418))),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(x418,s(*(x418,x418))),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(+(x418,x418)),*(x418,x418)) ↔ +(+(x418,x418),s(*(x418,x418))) ↔ +(x418,+(x418,s(*(x418,x418)))) ↔ +(+(x418,s(*(x418,x418))),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(x418,x418),s(*(x418,x418))) ↔ +(x418,+(x418,s(*(x418,x418)))) ↔ +(+(x418,s(*(x418,x418))),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(x418,s(*(x418,x418))),x418) ↔ +(+(x418,s(*(x418,x418))),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(x418,+(s(*(x418,x418)),x418)) ↔ +(+(x418,s(*(x418,x418))),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(x418,+(s(*(x418,x418)),x418)) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(x418,+(s(*(x418,x418)),x418)) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(x418,+(s(*(x418,x418)),x418)) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(+(x418,x418)),*(x418,x418)) ↔ +(+(x418,x418),s(*(x418,x418))) ↔ +(x418,+(x418,s(*(x418,x418)))) ↔ +(x418,+(s(*(x418,x418)),x418)) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(x418,x418),s(*(x418,x418))) ↔ +(x418,+(x418,s(*(x418,x418)))) ↔ +(x418,+(s(*(x418,x418)),x418)) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(x418,s(*(x418,x418))),x418) ↔ +(x418,+(s(*(x418,x418)),x418)) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(x418,+(s(*(x418,x418)),x418)) ↔ +(x418,+(s(*(x418,x418)),x418)) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(+(x418,x418)),*(x418,x418)) ↔ +(+(x418,x418),s(*(x418,x418))) ↔ +(x418,+(x418,s(*(x418,x418)))) ↔ +(x418,+(s(x418),*(x418,x418))) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(+(x418,x418)),*(x418,x418)) ↔ +(+(x418,x418),s(*(x418,x418))) ↔ +(x418,+(x418,s(*(x418,x418)))) ↔ +(x418,+(s(x418),*(x418,x418))) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(x418,x418),s(*(x418,x418))) ↔ +(x418,+(x418,s(*(x418,x418)))) ↔ +(x418,+(s(x418),*(x418,x418))) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(x418,x418),s(*(x418,x418))) ↔ +(x418,+(x418,s(*(x418,x418)))) ↔ +(x418,+(s(x418),*(x418,x418))) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(x418,s(*(x418,x418))),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(x418,s(*(x418,x418))),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(x418,s(*(x418,x418))),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(+(s(x418),*(x418,x418)),x418) ↔ +(s(x418),+(*(x418,x418),x418)) ↔ +(s(x418),*(s(x418),x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(x418,+(s(*(x418,x418)),x418)) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(x418,+(s(*(x418,x418)),x418)) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(x418,+(s(*(x418,x418)),x418)) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
-
The critical peak s = +(*(x418,x418),s(+(x418,x418)))←→ε *(s(x418),s(x418)) = t can be joined as follows.
s
↔ +(s(*(x418,x418)),+(x418,x418)) ↔ +(+(s(*(x418,x418)),x418),x418) ↔ +(+(*(x418,x418),s(x418)),x418) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(x418,+(*(x418,x418),s(x418))) ↔ +(+(x418,*(x418,x418)),s(x418)) ↔ +(*(x418,s(x418)),s(x418)) ↔
t
/>