Certification Problem
Input (COPS 200)
We consider the TRS containing the following rules:
|
+(x,0) |
→ |
x |
(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 2021)
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) |
|
+(x,0) |
→ |
x |
(1) |
|
+(0,x) |
→ |
x |
(4) |
|
+(s(y),x) |
→ |
s(+(y,x)) |
(5) |
|
+(s(x32),x) |
→ |
s(+(x32,x)) |
(6) |
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).
-
↦ 0
-
|
+(x,s(y)) |
→ |
s(+(y,x)) |
(2) |
↦ 1
-
↦ 0
-
↦ 0
-
|
+(s(y),x) |
→ |
s(+(y,x)) |
(5) |
↦ 1
-
|
+(s(x32),x) |
→ |
s(+(x32,x)) |
(6) |
↦ 2
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 = +(0,x)←→ε x = t can be joined as follows.
s
↔
t
-
The critical peak s = +(x,0)←→ε x = 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 = +(x,s(x32))←→ε s(+(x32,x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(x155,x))←→ε +(s(x155),x) = t can be joined as follows.
s
↔ s(+(x155,x)) ↔
t
-
The critical peak s = s(+(x157,0))←→ε s(x157) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(x159,s(y)))←→ε s(+(y,s(x159))) = t can be joined as follows.
s
↔ s(s(+(y,x159))) ↔ s(s(+(x159,y))) ↔
t
-
The critical peak s = s(+(x159,s(y)))←→ε s(+(y,s(x159))) = t can be joined as follows.
s
↔ s(+(s(y),x159)) ↔ s(s(+(y,x159))) ↔ s(s(+(x159,y))) ↔
t
-
The critical peak s = s(+(x159,s(y)))←→ε s(+(y,s(x159))) = t can be joined as follows.
s
↔ s(s(+(y,x159))) ↔ s(s(+(x159,y))) ↔
t
-
The critical peak s = s(+(x159,s(y)))←→ε s(+(y,s(x159))) = t can be joined as follows.
s
↔ s(s(+(y,x159))) ↔ s(s(+(x159,y))) ↔ s(+(s(x159),y)) ↔
t
-
The critical peak s = s(+(x161,s(x32)))←→ε s(+(x32,s(x161))) = t can be joined as follows.
s
↔ s(s(+(x32,x161))) ↔ s(s(+(x161,x32))) ↔
t
-
The critical peak s = s(+(x161,s(x32)))←→ε s(+(x32,s(x161))) = t can be joined as follows.
s
↔ s(+(s(x32),x161)) ↔ s(s(+(x32,x161))) ↔ s(s(+(x161,x32))) ↔
t
-
The critical peak s = s(+(x161,s(x32)))←→ε s(+(x32,s(x161))) = t can be joined as follows.
s
↔ s(s(+(x32,x161))) ↔ s(s(+(x161,x32))) ↔
t
-
The critical peak s = s(+(x161,s(x32)))←→ε s(+(x32,s(x161))) = t can be joined as follows.
s
↔ s(s(+(x32,x161))) ↔ s(s(+(x161,x32))) ↔ s(+(s(x161),x32)) ↔
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(y)←→ε s(+(y,0)) = t can be joined as follows.
s
↔ s(y) ↔
t
-
The critical peak s = s(x32)←→ε s(+(x32,0)) = t can be joined as follows.
s
↔ s(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 = 0←→ε 0 = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(x169,y))←→ε +(y,s(x169)) = t can be joined as follows.
s
↔ s(+(x169,y)) ↔
t
-
The critical peak s = s(+(x171,s(y)))←→ε s(+(y,s(x171))) = t can be joined as follows.
s
↔ s(s(+(y,x171))) ↔ s(s(+(x171,y))) ↔
t
-
The critical peak s = s(+(x171,s(y)))←→ε s(+(y,s(x171))) = t can be joined as follows.
s
↔ s(+(s(y),x171)) ↔ s(s(+(y,x171))) ↔ s(s(+(x171,y))) ↔
t
-
The critical peak s = s(+(x171,s(y)))←→ε s(+(y,s(x171))) = t can be joined as follows.
s
↔ s(s(+(y,x171))) ↔ s(s(+(x171,y))) ↔
t
-
The critical peak s = s(+(x171,s(y)))←→ε s(+(y,s(x171))) = t can be joined as follows.
s
↔ s(s(+(y,x171))) ↔ s(s(+(x171,y))) ↔ s(+(s(x171),y)) ↔
t
-
The critical peak s = s(+(x173,0))←→ε s(x173) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(x175,y))←→ε +(y,s(x175)) = t can be joined as follows.
s
↔ s(+(x175,y)) ↔
t
-
The critical peak s = s(+(x177,s(y)))←→ε s(+(y,s(x177))) = t can be joined as follows.
s
↔ s(s(+(y,x177))) ↔ s(s(+(x177,y))) ↔
t
-
The critical peak s = s(+(x177,s(y)))←→ε s(+(y,s(x177))) = t can be joined as follows.
s
↔ s(+(s(y),x177)) ↔ s(s(+(y,x177))) ↔ s(s(+(x177,y))) ↔
t
-
The critical peak s = s(+(x177,s(y)))←→ε s(+(y,s(x177))) = t can be joined as follows.
s
↔ s(s(+(y,x177))) ↔ s(s(+(x177,y))) ↔
t
-
The critical peak s = s(+(x177,s(y)))←→ε s(+(y,s(x177))) = t can be joined as follows.
s
↔ s(s(+(y,x177))) ↔ s(s(+(x177,y))) ↔ s(+(s(x177),y)) ↔
t
-
The critical peak s = s(+(x179,0))←→ε s(x179) = t can be joined as follows.
s
↔
t
/>