Certification Problem
Input (COPS 194)
We consider the TRS containing the following rules:
|
+(x,0) |
→ |
x |
(1) |
|
+(x,s(y)) |
→ |
s(+(x,y)) |
(2) |
|
*(x,0) |
→ |
0 |
(3) |
|
*(x,s(y)) |
→ |
+(*(x,y),x) |
(4) |
|
+(x,y) |
→ |
+(y,x) |
(5) |
The underlying signature is as follows:
{+/2, 0/0, s/1, */2}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by csi @ CoCo 2020)
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) |
(5) |
|
*(x,s(y)) |
→ |
+(*(x,y),x) |
(4) |
|
*(x,0) |
→ |
0 |
(3) |
|
+(x,s(y)) |
→ |
s(+(x,y)) |
(2) |
|
+(x,0) |
→ |
x |
(1) |
|
+(0,x) |
→ |
x |
(6) |
|
+(s(y),x) |
→ |
s(+(x,y)) |
(7) |
|
+(s(x79),x) |
→ |
s(+(x,x79)) |
(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).
-
↦ 0
-
|
*(x,s(y)) |
→ |
+(*(x,y),x) |
(4) |
↦ 0
-
↦ 0
-
|
+(x,s(y)) |
→ |
s(+(x,y)) |
(2) |
↦ 1
-
↦ 0
-
↦ 0
-
|
+(s(y),x) |
→ |
s(+(x,y)) |
(7) |
↦ 1
-
|
+(s(x79),x) |
→ |
s(+(x,x79)) |
(8) |
↦ 10
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(+(x,y)) = 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(+(x,y)) = t can be joined as follows.
s
↔
t
-
The critical peak s = +(x,s(x79))←→ε s(+(x,x79)) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(x,x287))←→ε +(s(x287),x) = t can be joined as follows.
s
↔ s(+(x,x287)) ↔
t
-
The critical peak s = s(+(0,x289))←→ε s(x289) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(s(y),x291))←→ε s(+(s(x291),y)) = t can be joined as follows.
s
↔ s(s(+(x291,y))) ↔ s(s(+(y,x291))) ↔
t
-
The critical peak s = s(+(s(y),x291))←→ε s(+(s(x291),y)) = t can be joined as follows.
s
↔ s(+(x291,s(y))) ↔ s(s(+(x291,y))) ↔ s(s(+(y,x291))) ↔
t
-
The critical peak s = s(+(s(y),x291))←→ε s(+(s(x291),y)) = t can be joined as follows.
s
↔ s(s(+(x291,y))) ↔ s(s(+(y,x291))) ↔
t
-
The critical peak s = s(+(s(y),x291))←→ε s(+(s(x291),y)) = t can be joined as follows.
s
↔ s(s(+(x291,y))) ↔ s(s(+(y,x291))) ↔ s(+(y,s(x291))) ↔
t
-
The critical peak s = s(+(s(x79),x293))←→ε s(+(s(x293),x79)) = t can be joined as follows.
s
↔ s(s(+(x293,x79))) ↔ s(s(+(x79,x293))) ↔
t
-
The critical peak s = s(+(s(x79),x293))←→ε s(+(s(x293),x79)) = t can be joined as follows.
s
↔ s(+(x293,s(x79))) ↔ s(s(+(x293,x79))) ↔ s(s(+(x79,x293))) ↔
t
-
The critical peak s = s(+(s(x79),x293))←→ε s(+(s(x293),x79)) = t can be joined as follows.
s
↔ s(s(+(x293,x79))) ↔ s(s(+(x79,x293))) ↔
t
-
The critical peak s = s(+(s(x79),x293))←→ε s(+(s(x293),x79)) = t can be joined as follows.
s
↔ s(s(+(x293,x79))) ↔ s(s(+(x79,x293))) ↔ s(+(x79,s(x293))) ↔
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(+(0,y)) = t can be joined as follows.
s
↔ s(y) ↔
t
-
The critical peak s = s(x79)←→ε s(+(0,x79)) = t can be joined as follows.
s
↔ s(x79) ↔
t
-
The critical peak s = y←→ε +(y,0) = t can be joined as follows.
s
↔ y ↔
t
-
The critical peak s = s(y)←→ε s(+(0,y)) = 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(+(y,x301))←→ε +(y,s(x301)) = t can be joined as follows.
s
↔ s(+(y,x301)) ↔
t
-
The critical peak s = s(+(s(y),x303))←→ε s(+(s(x303),y)) = t can be joined as follows.
s
↔ s(s(+(x303,y))) ↔ s(s(+(y,x303))) ↔
t
-
The critical peak s = s(+(s(y),x303))←→ε s(+(s(x303),y)) = t can be joined as follows.
s
↔ s(+(x303,s(y))) ↔ s(s(+(x303,y))) ↔ s(s(+(y,x303))) ↔
t
-
The critical peak s = s(+(s(y),x303))←→ε s(+(s(x303),y)) = t can be joined as follows.
s
↔ s(s(+(x303,y))) ↔ s(s(+(y,x303))) ↔
t
-
The critical peak s = s(+(s(y),x303))←→ε s(+(s(x303),y)) = t can be joined as follows.
s
↔ s(s(+(x303,y))) ↔ s(s(+(y,x303))) ↔ s(+(y,s(x303))) ↔
t
-
The critical peak s = s(+(0,x305))←→ε s(x305) = t can be joined as follows.
s
↔
t
-
The critical peak s = s(+(y,x307))←→ε +(y,s(x307)) = t can be joined as follows.
s
↔ s(+(y,x307)) ↔
t
-
The critical peak s = s(+(s(y),x309))←→ε s(+(s(x309),y)) = t can be joined as follows.
s
↔ s(s(+(x309,y))) ↔ s(s(+(y,x309))) ↔
t
-
The critical peak s = s(+(s(y),x309))←→ε s(+(s(x309),y)) = t can be joined as follows.
s
↔ s(+(x309,s(y))) ↔ s(s(+(x309,y))) ↔ s(s(+(y,x309))) ↔
t
-
The critical peak s = s(+(s(y),x309))←→ε s(+(s(x309),y)) = t can be joined as follows.
s
↔ s(s(+(x309,y))) ↔ s(s(+(y,x309))) ↔
t
-
The critical peak s = s(+(s(y),x309))←→ε s(+(s(x309),y)) = t can be joined as follows.
s
↔ s(s(+(x309,y))) ↔ s(s(+(y,x309))) ↔ s(+(y,s(x309))) ↔
t
-
The critical peak s = s(+(0,x311))←→ε s(x311) = t can be joined as follows.
s
↔
t
/>