Certification Problem
Input (COPS 180)
We consider the TRS containing the following rules:
|
+(0,y) |
→ |
y |
(1) |
|
+(x,s(y)) |
→ |
s(+(y,x)) |
(2) |
|
+(x,y) |
→ |
+(y,x) |
(3) |
The underlying signature is as follows:
{+/2, 0/0, s/1}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by csi @ CoCo 2023)
1 Redundant Rules Transformation
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following
modified system:
|
+(x,y) |
→ |
+(y,x) |
(3) |
|
+(x,s(y)) |
→ |
s(+(y,x)) |
(2) |
|
+(0,y) |
→ |
y |
(1) |
|
s(+(x34,0)) |
→ |
s(x34) |
(4) |
|
+(y,0) |
→ |
y |
(5) |
|
+(s(y),x) |
→ |
s(+(y,x)) |
(6) |
|
s(+(y,0)) |
→ |
s(y) |
(7) |
|
+(s(x32),x) |
→ |
s(+(x32,x)) |
(8) |
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).
-
↦ 1
-
|
+(x,s(y)) |
→ |
s(+(y,x)) |
(2) |
↦ 2
-
↦ 0
-
↦ 0
-
↦ 0
-
|
+(s(y),x) |
→ |
s(+(y,x)) |
(6) |
↦ 2
-
↦ 0
-
|
+(s(x32),x) |
→ |
s(+(x32,x)) |
(8) |
↦ 3
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 = +(s(y),x)←→ε s(+(y,x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = +(y,0)←→ε y = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(0,x34))←→ε s(x34) = t can be joined as follows.
s
↔
t
-
The critical peak s = +(0,y)←→ε y = t can be joined as follows.
s
↔
t
-
The critical peak s = +(x,s(y))←→ε s(+(y,x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(0,y))←→ε s(y) = t can be joined as follows.
s
↔
t
-
The critical peak s = +(x,s(x32))←→ε s(+(x32,x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(x256,x))←→ε +(s(x256),x) = t can be joined as follows.
s
↔ s(+(x256,x)) ↔
t
-
The critical peak s = s(+(x258,0))←→ε s(x258) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(x260,s(y)))←→ε s(+(y,s(x260))) = t can be joined as follows.
s
↔ s(s(+(y,x260))) ↔ s(s(+(x260,y))) ↔
t
-
The critical peak s = s(+(x260,s(y)))←→ε s(+(y,s(x260))) = t can be joined as follows.
s
↔ s(+(s(y),x260)) ↔ s(s(+(y,x260))) ↔ s(s(+(x260,y))) ↔
t
-
The critical peak s = s(+(x260,s(y)))←→ε s(+(y,s(x260))) = t can be joined as follows.
s
↔ s(s(+(y,x260))) ↔ s(s(+(x260,y))) ↔
t
-
The critical peak s = s(+(x260,s(y)))←→ε s(+(y,s(x260))) = t can be joined as follows.
s
↔ s(s(+(y,x260))) ↔ s(s(+(x260,y))) ↔ s(+(s(x260),y)) ↔
t
-
The critical peak s = s(+(x262,s(x32)))←→ε s(+(x32,s(x262))) = t can be joined as follows.
s
↔ s(s(+(x32,x262))) ↔ s(s(+(x262,x32))) ↔
t
-
The critical peak s = s(+(x262,s(x32)))←→ε s(+(x32,s(x262))) = t can be joined as follows.
s
↔ s(+(s(x32),x262)) ↔ s(s(+(x32,x262))) ↔ s(s(+(x262,x32))) ↔
t
-
The critical peak s = s(+(x262,s(x32)))←→ε s(+(x32,s(x262))) = t can be joined as follows.
s
↔ s(s(+(x32,x262))) ↔ s(s(+(x262,x32))) ↔
t
-
The critical peak s = s(+(x262,s(x32)))←→ε s(+(x32,s(x262))) = t can be joined as follows.
s
↔ s(s(+(x32,x262))) ↔ s(s(+(x262,x32))) ↔ s(+(s(x262),x32)) ↔
t
-
The critical peak s = y←→ε +(y,0) = t can be joined as follows.
s
↔ y ↔
t
-
The critical peak s = s(y)←→ε s(+(y,0)) = t can be joined as follows.
s
↔ s(y) ↔
t
-
The critical peak s = s(0)←→ε s(0) = t can be joined as follows.
s
↔
t
-
The critical peak s = 0←→ε 0 = t can be joined as follows.
s
↔
t
-
The critical peak s = s(0)←→ε s(0) = t can be joined as follows.
s
↔
t
-
The critical peak s = +(x,s(x268))←→ε s(+(+(x268,0),x)) = t can be joined as follows.
s
↔ s(+(x268,x)) ↔
t
-
The critical peak s = +(s(x269),x)←→ε s(+(+(x269,0),x)) = t can be joined as follows.
s
↔ s(+(x269,x)) ↔
t
-
The critical peak s = +(s(x270),x)←→ε s(+(+(x270,0),x)) = t can be joined as follows.
s
↔ s(+(x270,x)) ↔
t
-
The critical peak s = x←→ε +(0,x) = t can be joined as follows.
s
↔ x ↔
t
-
The critical peak s = 0←→ε 0 = t can be joined as follows.
s
↔
t
-
The critical peak s = s(x34)←→ε s(x34) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(y)←→ε s(+(y,0)) = t can be joined as follows.
s
↔ s(y) ↔
t
-
The critical peak s = s(y)←→ε s(y) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(x32)←→ε s(+(x32,0)) = t can be joined as follows.
s
↔ s(x32) ↔
t
-
The critical peak s = s(+(x277,y))←→ε +(y,s(x277)) = t can be joined as follows.
s
↔ s(+(x277,y)) ↔
t
-
The critical peak s = s(+(x279,s(y)))←→ε s(+(y,s(x279))) = t can be joined as follows.
s
↔ s(s(+(y,x279))) ↔ s(s(+(x279,y))) ↔
t
-
The critical peak s = s(+(x279,s(y)))←→ε s(+(y,s(x279))) = t can be joined as follows.
s
↔ s(+(s(y),x279)) ↔ s(s(+(y,x279))) ↔ s(s(+(x279,y))) ↔
t
-
The critical peak s = s(+(x279,s(y)))←→ε s(+(y,s(x279))) = t can be joined as follows.
s
↔ s(s(+(y,x279))) ↔ s(s(+(x279,y))) ↔
t
-
The critical peak s = s(+(x279,s(y)))←→ε s(+(y,s(x279))) = t can be joined as follows.
s
↔ s(s(+(y,x279))) ↔ s(s(+(x279,y))) ↔ s(+(s(x279),y)) ↔
t
-
The critical peak s = s(s(+(x281,0)))←→ε s(s(x281)) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(x283,0))←→ε s(x283) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(s(+(x285,0)))←→ε s(s(x285)) = t can be joined as follows.
s
↔
t
-
The critical peak s = +(x,s(x287))←→ε s(+(+(x287,0),x)) = t can be joined as follows.
s
↔ s(+(x287,x)) ↔
t
-
The critical peak s = +(s(x288),x)←→ε s(+(+(x288,0),x)) = t can be joined as follows.
s
↔ s(+(x288,x)) ↔
t
-
The critical peak s = +(s(x289),x)←→ε s(+(+(x289,0),x)) = t can be joined as follows.
s
↔ s(+(x289,x)) ↔
t
-
The critical peak s = s(+(x290,y))←→ε +(y,s(x290)) = t can be joined as follows.
s
↔ s(+(x290,y)) ↔
t
-
The critical peak s = s(+(x292,s(y)))←→ε s(+(y,s(x292))) = t can be joined as follows.
s
↔ s(s(+(y,x292))) ↔ s(s(+(x292,y))) ↔
t
-
The critical peak s = s(+(x292,s(y)))←→ε s(+(y,s(x292))) = t can be joined as follows.
s
↔ s(+(s(y),x292)) ↔ s(s(+(y,x292))) ↔ s(s(+(x292,y))) ↔
t
-
The critical peak s = s(+(x292,s(y)))←→ε s(+(y,s(x292))) = t can be joined as follows.
s
↔ s(s(+(y,x292))) ↔ s(s(+(x292,y))) ↔
t
-
The critical peak s = s(+(x292,s(y)))←→ε s(+(y,s(x292))) = t can be joined as follows.
s
↔ s(s(+(y,x292))) ↔ s(s(+(x292,y))) ↔ s(+(s(x292),y)) ↔
t
-
The critical peak s = s(s(+(x294,0)))←→ε s(s(x294)) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(x296,0))←→ε s(x296) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(s(+(x298,0)))←→ε s(s(x298)) = t can be joined as follows.
s
↔
t
/>