Certification Problem
Input (COPS 146)
We consider the TRS containing the following rules:
|
+(x,0) |
→ |
x |
(1) |
|
+(s(x),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) |
|
+(s(x),y) |
→ |
s(+(y,x)) |
(2) |
|
+(x,0) |
→ |
x |
(1) |
|
s(+(0,x33)) |
→ |
s(x33) |
(4) |
|
+(0,x) |
→ |
x |
(5) |
|
+(y,s(x)) |
→ |
s(+(y,x)) |
(6) |
|
s(+(0,x)) |
→ |
s(x) |
(7) |
|
+(y,s(x31)) |
→ |
s(+(y,x31)) |
(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
-
|
+(s(x),y) |
→ |
s(+(y,x)) |
(2) |
↦ 2
-
↦ 0
-
↦ 0
-
↦ 0
-
|
+(y,s(x)) |
→ |
s(+(y,x)) |
(6) |
↦ 2
-
↦ 0
-
|
+(y,s(x31)) |
→ |
s(+(y,x31)) |
(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 = +(y,s(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 = s(+(x33,0))←→ε s(x33) = 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 = +(s(x),y)←→ε s(+(y,x)) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(x,0))←→ε s(x) = t can be joined as follows.
s
↔
t
-
The critical peak s = +(s(x31),y)←→ε s(+(y,x31)) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(y,x255))←→ε +(y,s(x255)) = t can be joined as follows.
s
↔ s(+(y,x255)) ↔
t
-
The critical peak s = s(+(0,x257))←→ε s(x257) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(s(x),x259))←→ε s(+(s(x259),x)) = t can be joined as follows.
s
↔ s(s(+(x259,x))) ↔ s(s(+(x,x259))) ↔
t
-
The critical peak s = s(+(s(x),x259))←→ε s(+(s(x259),x)) = t can be joined as follows.
s
↔ s(+(x259,s(x))) ↔ s(s(+(x259,x))) ↔ s(s(+(x,x259))) ↔
t
-
The critical peak s = s(+(s(x),x259))←→ε s(+(s(x259),x)) = t can be joined as follows.
s
↔ s(s(+(x259,x))) ↔ s(s(+(x,x259))) ↔
t
-
The critical peak s = s(+(s(x),x259))←→ε s(+(s(x259),x)) = t can be joined as follows.
s
↔ s(s(+(x259,x))) ↔ s(s(+(x,x259))) ↔ s(+(x,s(x259))) ↔
t
-
The critical peak s = s(+(s(x31),x261))←→ε s(+(s(x261),x31)) = t can be joined as follows.
s
↔ s(s(+(x261,x31))) ↔ s(s(+(x31,x261))) ↔
t
-
The critical peak s = s(+(s(x31),x261))←→ε s(+(s(x261),x31)) = t can be joined as follows.
s
↔ s(+(x261,s(x31))) ↔ s(s(+(x261,x31))) ↔ s(s(+(x31,x261))) ↔
t
-
The critical peak s = s(+(s(x31),x261))←→ε s(+(s(x261),x31)) = t can be joined as follows.
s
↔ s(s(+(x261,x31))) ↔ s(s(+(x31,x261))) ↔
t
-
The critical peak s = s(+(s(x31),x261))←→ε s(+(s(x261),x31)) = t can be joined as follows.
s
↔ s(s(+(x261,x31))) ↔ s(s(+(x31,x261))) ↔ s(+(x31,s(x261))) ↔
t
-
The critical peak s = x←→ε +(0,x) = t can be joined as follows.
s
↔ x ↔
t
-
The critical peak s = s(x)←→ε s(+(0,x)) = t can be joined as follows.
s
↔ s(x) ↔
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 = +(s(x268),y)←→ε s(+(y,+(0,x268))) = t can be joined as follows.
s
↔ s(+(y,x268)) ↔
t
-
The critical peak s = +(y,s(x269))←→ε s(+(y,+(0,x269))) = t can be joined as follows.
s
↔ s(+(y,x269)) ↔
t
-
The critical peak s = +(y,s(x270))←→ε s(+(y,+(0,x270))) = t can be joined as follows.
s
↔ s(+(y,x270)) ↔
t
-
The critical peak s = y←→ε +(y,0) = t can be joined as follows.
s
↔ y ↔
t
-
The critical peak s = 0←→ε 0 = t can be joined as follows.
s
↔
t
-
The critical peak s = s(x33)←→ε s(x33) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(x)←→ε s(+(0,x)) = t can be joined as follows.
s
↔ s(x) ↔
t
-
The critical peak s = s(x)←→ε s(x) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(x31)←→ε s(+(0,x31)) = t can be joined as follows.
s
↔ s(x31) ↔
t
-
The critical peak s = s(+(x,x278))←→ε +(s(x278),x) = t can be joined as follows.
s
↔ s(+(x,x278)) ↔
t
-
The critical peak s = s(+(s(x),x280))←→ε s(+(s(x280),x)) = t can be joined as follows.
s
↔ s(s(+(x280,x))) ↔ s(s(+(x,x280))) ↔
t
-
The critical peak s = s(+(s(x),x280))←→ε s(+(s(x280),x)) = t can be joined as follows.
s
↔ s(+(x280,s(x))) ↔ s(s(+(x280,x))) ↔ s(s(+(x,x280))) ↔
t
-
The critical peak s = s(+(s(x),x280))←→ε s(+(s(x280),x)) = t can be joined as follows.
s
↔ s(s(+(x280,x))) ↔ s(s(+(x,x280))) ↔
t
-
The critical peak s = s(+(s(x),x280))←→ε s(+(s(x280),x)) = t can be joined as follows.
s
↔ s(s(+(x280,x))) ↔ s(s(+(x,x280))) ↔ s(+(x,s(x280))) ↔
t
-
The critical peak s = s(s(+(0,x282)))←→ε s(s(x282)) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(0,x284))←→ε s(x284) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(s(+(0,x286)))←→ε s(s(x286)) = t can be joined as follows.
s
↔
t
-
The critical peak s = +(s(x287),y)←→ε s(+(y,+(0,x287))) = t can be joined as follows.
s
↔ s(+(y,x287)) ↔
t
-
The critical peak s = +(y,s(x288))←→ε s(+(y,+(0,x288))) = t can be joined as follows.
s
↔ s(+(y,x288)) ↔
t
-
The critical peak s = +(y,s(x289))←→ε s(+(y,+(0,x289))) = t can be joined as follows.
s
↔ s(+(y,x289)) ↔
t
-
The critical peak s = s(+(x,x291))←→ε +(s(x291),x) = t can be joined as follows.
s
↔ s(+(x,x291)) ↔
t
-
The critical peak s = s(+(s(x),x293))←→ε s(+(s(x293),x)) = t can be joined as follows.
s
↔ s(s(+(x293,x))) ↔ s(s(+(x,x293))) ↔
t
-
The critical peak s = s(+(s(x),x293))←→ε s(+(s(x293),x)) = t can be joined as follows.
s
↔ s(+(x293,s(x))) ↔ s(s(+(x293,x))) ↔ s(s(+(x,x293))) ↔
t
-
The critical peak s = s(+(s(x),x293))←→ε s(+(s(x293),x)) = t can be joined as follows.
s
↔ s(s(+(x293,x))) ↔ s(s(+(x,x293))) ↔
t
-
The critical peak s = s(+(s(x),x293))←→ε s(+(s(x293),x)) = t can be joined as follows.
s
↔ s(s(+(x293,x))) ↔ s(s(+(x,x293))) ↔ s(+(x,s(x293))) ↔
t
-
The critical peak s = s(s(+(0,x295)))←→ε s(s(x295)) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(0,x297))←→ε s(x297) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(s(+(0,x299)))←→ε s(s(x299)) = t can be joined as follows.
s
↔
t
/>