YES
Confluence Proof
Confluence Proof
by csi
Input
The rewrite relation of the following TRS is considered.
|
E(+(x,y)) |
→ |
*(E(x),E(y)) |
|
E(0) |
→ |
1 |
|
+(x,0) |
→ |
x |
|
+(0,x) |
→ |
x |
|
*(x,1) |
→ |
x |
|
*(1,x) |
→ |
x |
|
+(+(x,y),z) |
→ |
+(x,+(y,z)) |
|
+(x,+(y,z)) |
→ |
+(+(x,y),z) |
|
+(x,y) |
→ |
+(y,x) |
|
*(*(x,y),z) |
→ |
*(x,*(y,z)) |
|
*(x,*(y,z)) |
→ |
*(*(x,y),z) |
|
*(x,y) |
→ |
*(y,x) |
Proof
1 Decreasing Diagrams
1.1 Relative Termination Proof
The duplicating rules (R) terminate relative to the other rules (S).
1.1.1 R is empty
There are no rules in the TRS R. Hence, R/S is relative terminating.
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)) ↦ 0
-
E(0)→1 ↦ 1
-
+(x,0)→x ↦ 1
-
+(0,x)→x ↦ 1
-
*(x,1)→x ↦ 0
-
*(1,x)→x ↦ 0
-
+(+(x,y),z)→+(x,+(y,z)) ↦ 1
-
+(x,+(y,z))→+(+(x,y),z) ↦ 1
-
+(x,y)→+(y,x) ↦ 1
-
*(*(x,y),z)→*(x,*(y,z)) ↦ 0
-
*(x,*(y,z))→*(*(x,y),z) ↦ 0
-
*(x,y)→*(y,x) ↦ 0
All critical pairs are joinable:
-
E(x)←*(E(x),1)←*(E(x),E(0))
- 0
-
+(x,y)←+(x,+(y,0))
-
+(x,z)←+(x,+(0,z))
-
+(x,y)←+(+(x,y),0)
-
x←+(0,x)
-
E(y)←*(1,E(y))←*(E(0),E(y))
- 0
-
+(y,z)←+(0,+(y,z))
-
+(y,z)←+(+(0,y),z)
-
+(x,z)←+(+(x,0),z)
-
y←+(y,0)
- 1
-
*(x,y)←*(x,*(y,1))
-
*(x,z)←*(x,*(1,z))
-
*(x,y)←*(*(x,y),1)
-
x←*(1,x)
- 1
-
*(y,z)←*(1,*(y,z))
-
*(y,z)←*(*(1,y),z)
-
*(x,z)←*(*(x,1),z)
-
y←*(y,1)
-
E(+(x509,+(x510,y)))→*(E(x509),E(+(x510,y)))→*(E(x509),*(E(x510),E(y)))←*(*(E(x509),E(x510)),E(y))←*(E(+(x509,x510)),E(y))
-
E(+(x509,+(x510,y)))→E(+(+(x509,x510),y))→*(E(+(x509,x510)),E(y))
-
+(x512,+(x513,0))→+(x512,x513)
-
+(+(x515,+(x516,y)),z)→+(+(+(x515,x516),y),z)←+(+(x515,x516),+(y,z))
-
+(x518,+(x519,+(y,z)))→+(+(x518,x519),+(y,z))←+(+(+(x518,x519),y),z)
-
+(x,+(x521,+(x522,z)))→+(x,+(+(x521,x522),z))←+(+(x,+(x521,x522)),z)
-
+(x524,+(x525,y))→+(+(x524,x525),y)←+(y,+(x524,x525))
-
E(+(+(x,x528),x529))→*(E(+(x,x528)),E(x529))→*(*(E(x),E(x528)),E(x529))←*(E(x),*(E(x528),E(x529)))←*(E(x),E(+(x528,x529)))
-
E(+(+(x,x528),x529))→E(+(x,+(x528,x529)))→*(E(x),E(+(x528,x529)))
-
+(+(0,x531),x532)→+(x531,x532)
-
+(+(+(x,y),x534),x535)→+(+(x,y),+(x534,x535))←+(x,+(y,+(x534,x535)))
-
+(+(+(x,x537),x538),z)→+(+(x,+(x537,x538)),z)←+(x,+(+(x537,x538),z))
-
+(x,+(+(y,x540),x541))→+(x,+(y,+(x540,x541)))←+(+(x,y),+(x540,x541))
-
+(+(x,x543),x544)→+(x,+(x543,x544))←+(+(x543,x544),x)
-
E(+(y,x))→*(E(y),E(x))←*(E(x),E(y))
-
+(0,x)→x
-
+(x,0)→x
-
+(z,+(x,y))→+(+(x,y),z)←+(x,+(y,z))
-
+(+(y,x),z)→+(+(x,y),z)←+(x,+(y,z))
-
+(+(y,z),x)→+(x,+(y,z))←+(+(x,y),z)
-
+(x,+(z,y))→+(x,+(y,z))←+(+(x,y),z)
-
*(x559,*(x560,1))→*(x559,x560)
-
*(*(x562,*(x563,y)),z)→*(*(*(x562,x563),y),z)←*(*(x562,x563),*(y,z))
-
*(x565,*(x566,*(y,z)))→*(*(x565,x566),*(y,z))←*(*(*(x565,x566),y),z)
-
*(x,*(x568,*(x569,z)))→*(x,*(*(x568,x569),z))←*(*(x,*(x568,x569)),z)
-
*(x571,*(x572,y))→*(*(x571,x572),y)←*(y,*(x571,x572))
-
*(*(1,x575),x576)→*(x575,x576)
-
*(*(*(x,y),x578),x579)→*(*(x,y),*(x578,x579))←*(x,*(y,*(x578,x579)))
-
*(*(*(x,x581),x582),z)→*(*(x,*(x581,x582)),z)←*(x,*(*(x581,x582),z))
-
*(x,*(*(y,x584),x585))→*(x,*(y,*(x584,x585)))←*(*(x,y),*(x584,x585))
-
*(*(x,x587),x588)→*(x,*(x587,x588))←*(*(x587,x588),x)
-
*(1,x)→x
-
*(x,1)→x
-
*(z,*(x,y))→*(*(x,y),z)←*(x,*(y,z))
-
*(*(y,x),z)→*(*(x,y),z)←*(x,*(y,z))
-
*(*(y,z),x)→*(x,*(y,z))←*(*(x,y),z)
-
*(x,*(z,y))→*(x,*(y,z))←*(*(x,y),z)
Tool configuration
csi
- version: csi 1.2.5 [hg: unknown]
- strategy:
(if linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)!