Certification Problem
Input (COPS 530)
We consider the TRS containing the following rules:
|
E(+(x,y)) |
→ |
*(E(x),E(y)) |
(1) |
|
E(0) |
→ |
1 |
(2) |
|
+(x,0) |
→ |
x |
(3) |
|
+(0,x) |
→ |
x |
(4) |
|
*(x,1) |
→ |
x |
(5) |
|
*(1,x) |
→ |
x |
(6) |
|
+(+(x,y),z) |
→ |
+(x,+(y,z)) |
(7) |
|
+(x,+(y,z)) |
→ |
+(+(x,y),z) |
(8) |
|
+(x,y) |
→ |
+(y,x) |
(9) |
|
*(*(x,y),z) |
→ |
*(x,*(y,z)) |
(10) |
|
*(x,*(y,z)) |
→ |
*(*(x,y),z) |
(11) |
|
*(x,y) |
→ |
*(y,x) |
(12) |
The underlying signature is as follows:
{E/1, +/2, */2, 0/0, 1/0}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by csi @ CoCo 2021)
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).
-
|
E(+(x,y)) |
→ |
*(E(x),E(y)) |
(1) |
↦ 0
-
↦ 1
-
↦ 1
-
↦ 1
-
↦ 0
-
↦ 0
-
|
+(+(x,y),z) |
→ |
+(x,+(y,z)) |
(7) |
↦ 1
-
|
+(x,+(y,z)) |
→ |
+(+(x,y),z) |
(8) |
↦ 1
-
↦ 1
-
|
*(*(x,y),z) |
→ |
*(x,*(y,z)) |
(10) |
↦ 0
-
|
*(x,*(y,z)) |
→ |
*(*(x,y),z) |
(11) |
↦ 0
-
↦ 0
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 = E(x)←→ε *(E(x),E(0)) = t can be joined as follows.
s
↔ E(x) ↔ *(E(x),1) ↔
t
-
The critical peak s = 0←→ε 0 = t can be joined as follows.
s
↔
t
-
The critical peak s = +(x,y)←→ε +(x,+(y,0)) = t can be joined as follows.
s
↔ +(x,y) ↔
t
-
The critical peak s = +(x,z)←→ε +(x,+(0,z)) = t can be joined as follows.
s
↔ +(x,z) ↔
t
-
The critical peak s = +(x,y)←→ε +(+(x,y),0) = t can be joined as follows.
s
↔ +(x,y) ↔
t
-
The critical peak s = x←→ε +(0,x) = t can be joined as follows.
s
↔ x ↔
t
-
The critical peak s = E(y)←→ε *(E(0),E(y)) = t can be joined as follows.
s
↔ E(y) ↔ *(1,E(y)) ↔
t
-
The critical peak s = 0←→ε 0 = t can be joined as follows.
s
↔
t
-
The critical peak s = +(y,z)←→ε +(0,+(y,z)) = t can be joined as follows.
s
↔ +(y,z) ↔
t
-
The critical peak s = +(y,z)←→ε +(+(0,y),z) = t can be joined as follows.
s
↔ +(y,z) ↔
t
-
The critical peak s = +(x,z)←→ε +(+(x,0),z) = t can be joined as follows.
s
↔ +(x,z) ↔
t
-
The critical peak s = y←→ε +(y,0) = t can be joined as follows.
s
↔ y ↔
t
-
The critical peak s = 1←→ε 1 = t can be joined as follows.
s
↔
t
-
The critical peak s = *(x,y)←→ε *(x,*(y,1)) = t can be joined as follows.
s
↔ *(x,y) ↔
t
-
The critical peak s = *(x,z)←→ε *(x,*(1,z)) = t can be joined as follows.
s
↔ *(x,z) ↔
t
-
The critical peak s = *(x,y)←→ε *(*(x,y),1) = t can be joined as follows.
s
↔ *(x,y) ↔
t
-
The critical peak s = x←→ε *(1,x) = t can be joined as follows.
s
↔ x ↔
t
-
The critical peak s = 1←→ε 1 = t can be joined as follows.
s
↔
t
-
The critical peak s = *(y,z)←→ε *(1,*(y,z)) = t can be joined as follows.
s
↔ *(y,z) ↔
t
-
The critical peak s = *(y,z)←→ε *(*(1,y),z) = t can be joined as follows.
s
↔ *(y,z) ↔
t
-
The critical peak s = *(x,z)←→ε *(*(x,1),z) = t can be joined as follows.
s
↔ *(x,z) ↔
t
-
The critical peak s = y←→ε *(y,1) = t can be joined as follows.
s
↔ y ↔
t
-
The critical peak s = E(+(x509,+(x510,y)))←→ε *(E(+(x509,x510)),E(y)) = t can be joined as follows.
s
↔ *(E(x509),E(+(x510,y))) ↔ *(E(x509),*(E(x510),E(y))) ↔ *(*(E(x509),E(x510)),E(y)) ↔
t
-
The critical peak s = E(+(x509,+(x510,y)))←→ε *(E(+(x509,x510)),E(y)) = t can be joined as follows.
s
↔ E(+(+(x509,x510),y)) ↔
t
-
The critical peak s = +(x512,+(x513,0))←→ε +(x512,x513) = t can be joined as follows.
s
↔
t
-
The critical peak s = +(+(x515,+(x516,y)),z)←→ε +(+(x515,x516),+(y,z)) = t can be joined as follows.
s
↔ +(+(+(x515,x516),y),z) ↔
t
-
The critical peak s = +(x518,+(x519,+(y,z)))←→ε +(+(+(x518,x519),y),z) = t can be joined as follows.
s
↔ +(+(x518,x519),+(y,z)) ↔
t
-
The critical peak s = +(x,+(x521,+(x522,z)))←→ε +(+(x,+(x521,x522)),z) = t can be joined as follows.
s
↔ +(x,+(+(x521,x522),z)) ↔
t
-
The critical peak s = +(x524,+(x525,y))←→ε +(y,+(x524,x525)) = t can be joined as follows.
s
↔ +(+(x524,x525),y) ↔
t
-
The critical peak s = E(+(+(x,x528),x529))←→ε *(E(x),E(+(x528,x529))) = t can be joined as follows.
s
↔ *(E(+(x,x528)),E(x529)) ↔ *(*(E(x),E(x528)),E(x529)) ↔ *(E(x),*(E(x528),E(x529))) ↔
t
-
The critical peak s = E(+(+(x,x528),x529))←→ε *(E(x),E(+(x528,x529))) = t can be joined as follows.
s
↔ E(+(x,+(x528,x529))) ↔
t
-
The critical peak s = +(+(0,x531),x532)←→ε +(x531,x532) = t can be joined as follows.
s
↔
t
-
The critical peak s = +(+(+(x,y),x534),x535)←→ε +(x,+(y,+(x534,x535))) = t can be joined as follows.
s
↔ +(+(x,y),+(x534,x535)) ↔
t
-
The critical peak s = +(+(+(x,x537),x538),z)←→ε +(x,+(+(x537,x538),z)) = t can be joined as follows.
s
↔ +(+(x,+(x537,x538)),z) ↔
t
-
The critical peak s = +(x,+(+(y,x540),x541))←→ε +(+(x,y),+(x540,x541)) = t can be joined as follows.
s
↔ +(x,+(y,+(x540,x541))) ↔
t
-
The critical peak s = +(+(x,x543),x544)←→ε +(+(x543,x544),x) = t can be joined as follows.
s
↔ +(x,+(x543,x544)) ↔
t
-
The critical peak s = E(+(y,x))←→ε *(E(x),E(y)) = t can be joined as follows.
s
↔ *(E(y),E(x)) ↔
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 = +(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,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 = *(x559,*(x560,1))←→ε *(x559,x560) = t can be joined as follows.
s
↔
t
-
The critical peak s = *(*(x562,*(x563,y)),z)←→ε *(*(x562,x563),*(y,z)) = t can be joined as follows.
s
↔ *(*(*(x562,x563),y),z) ↔
t
-
The critical peak s = *(x565,*(x566,*(y,z)))←→ε *(*(*(x565,x566),y),z) = t can be joined as follows.
s
↔ *(*(x565,x566),*(y,z)) ↔
t
-
The critical peak s = *(x,*(x568,*(x569,z)))←→ε *(*(x,*(x568,x569)),z) = t can be joined as follows.
s
↔ *(x,*(*(x568,x569),z)) ↔
t
-
The critical peak s = *(x571,*(x572,y))←→ε *(y,*(x571,x572)) = t can be joined as follows.
s
↔ *(*(x571,x572),y) ↔
t
-
The critical peak s = *(*(1,x575),x576)←→ε *(x575,x576) = t can be joined as follows.
s
↔
t
-
The critical peak s = *(*(*(x,y),x578),x579)←→ε *(x,*(y,*(x578,x579))) = t can be joined as follows.
s
↔ *(*(x,y),*(x578,x579)) ↔
t
-
The critical peak s = *(*(*(x,x581),x582),z)←→ε *(x,*(*(x581,x582),z)) = t can be joined as follows.
s
↔ *(*(x,*(x581,x582)),z) ↔
t
-
The critical peak s = *(x,*(*(y,x584),x585))←→ε *(*(x,y),*(x584,x585)) = t can be joined as follows.
s
↔ *(x,*(y,*(x584,x585))) ↔
t
-
The critical peak s = *(*(x,x587),x588)←→ε *(*(x587,x588),x) = t can be joined as follows.
s
↔ *(x,*(x587,x588)) ↔
t
-
The critical peak s = *(1,x)←→ε x = t can be joined as follows.
s
↔
t
-
The critical peak s = *(x,1)←→ε x = t can be joined as follows.
s
↔
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,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
/>