The rewrite relation of the following TRS is considered.
active(from(X)) |
→ |
mark(cons(X,from(s(X)))) |
(1) |
active(2ndspos(0,Z)) |
→ |
mark(rnil) |
(2) |
active(2ndspos(s(N),cons(X,cons(Y,Z)))) |
→ |
mark(rcons(posrecip(Y),2ndsneg(N,Z))) |
(3) |
active(2ndsneg(0,Z)) |
→ |
mark(rnil) |
(4) |
active(2ndsneg(s(N),cons(X,cons(Y,Z)))) |
→ |
mark(rcons(negrecip(Y),2ndspos(N,Z))) |
(5) |
active(pi(X)) |
→ |
mark(2ndspos(X,from(0))) |
(6) |
active(plus(0,Y)) |
→ |
mark(Y) |
(7) |
active(plus(s(X),Y)) |
→ |
mark(s(plus(X,Y))) |
(8) |
active(times(0,Y)) |
→ |
mark(0) |
(9) |
active(times(s(X),Y)) |
→ |
mark(plus(Y,times(X,Y))) |
(10) |
active(square(X)) |
→ |
mark(times(X,X)) |
(11) |
mark(from(X)) |
→ |
active(from(mark(X))) |
(12) |
mark(cons(X1,X2)) |
→ |
active(cons(mark(X1),X2)) |
(13) |
mark(s(X)) |
→ |
active(s(mark(X))) |
(14) |
mark(2ndspos(X1,X2)) |
→ |
active(2ndspos(mark(X1),mark(X2))) |
(15) |
mark(0) |
→ |
active(0) |
(16) |
mark(rnil) |
→ |
active(rnil) |
(17) |
mark(rcons(X1,X2)) |
→ |
active(rcons(mark(X1),mark(X2))) |
(18) |
mark(posrecip(X)) |
→ |
active(posrecip(mark(X))) |
(19) |
mark(2ndsneg(X1,X2)) |
→ |
active(2ndsneg(mark(X1),mark(X2))) |
(20) |
mark(negrecip(X)) |
→ |
active(negrecip(mark(X))) |
(21) |
mark(pi(X)) |
→ |
active(pi(mark(X))) |
(22) |
mark(plus(X1,X2)) |
→ |
active(plus(mark(X1),mark(X2))) |
(23) |
mark(times(X1,X2)) |
→ |
active(times(mark(X1),mark(X2))) |
(24) |
mark(square(X)) |
→ |
active(square(mark(X))) |
(25) |
from(mark(X)) |
→ |
from(X) |
(26) |
from(active(X)) |
→ |
from(X) |
(27) |
cons(mark(X1),X2) |
→ |
cons(X1,X2) |
(28) |
cons(X1,mark(X2)) |
→ |
cons(X1,X2) |
(29) |
cons(active(X1),X2) |
→ |
cons(X1,X2) |
(30) |
cons(X1,active(X2)) |
→ |
cons(X1,X2) |
(31) |
s(mark(X)) |
→ |
s(X) |
(32) |
s(active(X)) |
→ |
s(X) |
(33) |
2ndspos(mark(X1),X2) |
→ |
2ndspos(X1,X2) |
(34) |
2ndspos(X1,mark(X2)) |
→ |
2ndspos(X1,X2) |
(35) |
2ndspos(active(X1),X2) |
→ |
2ndspos(X1,X2) |
(36) |
2ndspos(X1,active(X2)) |
→ |
2ndspos(X1,X2) |
(37) |
rcons(mark(X1),X2) |
→ |
rcons(X1,X2) |
(38) |
rcons(X1,mark(X2)) |
→ |
rcons(X1,X2) |
(39) |
rcons(active(X1),X2) |
→ |
rcons(X1,X2) |
(40) |
rcons(X1,active(X2)) |
→ |
rcons(X1,X2) |
(41) |
posrecip(mark(X)) |
→ |
posrecip(X) |
(42) |
posrecip(active(X)) |
→ |
posrecip(X) |
(43) |
2ndsneg(mark(X1),X2) |
→ |
2ndsneg(X1,X2) |
(44) |
2ndsneg(X1,mark(X2)) |
→ |
2ndsneg(X1,X2) |
(45) |
2ndsneg(active(X1),X2) |
→ |
2ndsneg(X1,X2) |
(46) |
2ndsneg(X1,active(X2)) |
→ |
2ndsneg(X1,X2) |
(47) |
negrecip(mark(X)) |
→ |
negrecip(X) |
(48) |
negrecip(active(X)) |
→ |
negrecip(X) |
(49) |
pi(mark(X)) |
→ |
pi(X) |
(50) |
pi(active(X)) |
→ |
pi(X) |
(51) |
plus(mark(X1),X2) |
→ |
plus(X1,X2) |
(52) |
plus(X1,mark(X2)) |
→ |
plus(X1,X2) |
(53) |
plus(active(X1),X2) |
→ |
plus(X1,X2) |
(54) |
plus(X1,active(X2)) |
→ |
plus(X1,X2) |
(55) |
times(mark(X1),X2) |
→ |
times(X1,X2) |
(56) |
times(X1,mark(X2)) |
→ |
times(X1,X2) |
(57) |
times(active(X1),X2) |
→ |
times(X1,X2) |
(58) |
times(X1,active(X2)) |
→ |
times(X1,X2) |
(59) |
square(mark(X)) |
→ |
square(X) |
(60) |
square(active(X)) |
→ |
square(X) |
(61) |
There are 106 ruless (increase limit for explicit display).
The dependency pairs are split into 13
components.
-
The
1st
component contains the
pair
mark#(from(X)) |
→ |
active#(from(mark(X))) |
(89) |
active#(from(X)) |
→ |
mark#(cons(X,from(s(X)))) |
(62) |
mark#(from(X)) |
→ |
mark#(X) |
(91) |
mark#(cons(X1,X2)) |
→ |
active#(cons(mark(X1),X2)) |
(92) |
active#(2ndspos(s(N),cons(X,cons(Y,Z)))) |
→ |
mark#(rcons(posrecip(Y),2ndsneg(N,Z))) |
(67) |
mark#(cons(X1,X2)) |
→ |
mark#(X1) |
(94) |
mark#(s(X)) |
→ |
active#(s(mark(X))) |
(95) |
active#(2ndsneg(s(N),cons(X,cons(Y,Z)))) |
→ |
mark#(rcons(negrecip(Y),2ndspos(N,Z))) |
(72) |
mark#(s(X)) |
→ |
mark#(X) |
(97) |
mark#(2ndspos(X1,X2)) |
→ |
active#(2ndspos(mark(X1),mark(X2))) |
(98) |
active#(pi(X)) |
→ |
mark#(2ndspos(X,from(0))) |
(76) |
mark#(2ndspos(X1,X2)) |
→ |
mark#(X1) |
(100) |
mark#(2ndspos(X1,X2)) |
→ |
mark#(X2) |
(101) |
mark#(rcons(X1,X2)) |
→ |
active#(rcons(mark(X1),mark(X2))) |
(104) |
active#(plus(0,Y)) |
→ |
mark#(Y) |
(79) |
mark#(rcons(X1,X2)) |
→ |
mark#(X1) |
(106) |
mark#(rcons(X1,X2)) |
→ |
mark#(X2) |
(107) |
mark#(posrecip(X)) |
→ |
active#(posrecip(mark(X))) |
(108) |
active#(plus(s(X),Y)) |
→ |
mark#(s(plus(X,Y))) |
(80) |
mark#(posrecip(X)) |
→ |
mark#(X) |
(110) |
mark#(2ndsneg(X1,X2)) |
→ |
active#(2ndsneg(mark(X1),mark(X2))) |
(111) |
active#(times(s(X),Y)) |
→ |
mark#(plus(Y,times(X,Y))) |
(84) |
mark#(2ndsneg(X1,X2)) |
→ |
mark#(X1) |
(113) |
mark#(2ndsneg(X1,X2)) |
→ |
mark#(X2) |
(114) |
mark#(negrecip(X)) |
→ |
active#(negrecip(mark(X))) |
(115) |
active#(square(X)) |
→ |
mark#(times(X,X)) |
(87) |
mark#(negrecip(X)) |
→ |
mark#(X) |
(117) |
mark#(pi(X)) |
→ |
active#(pi(mark(X))) |
(118) |
mark#(pi(X)) |
→ |
mark#(X) |
(120) |
mark#(plus(X1,X2)) |
→ |
active#(plus(mark(X1),mark(X2))) |
(121) |
mark#(plus(X1,X2)) |
→ |
mark#(X1) |
(123) |
mark#(plus(X1,X2)) |
→ |
mark#(X2) |
(124) |
mark#(times(X1,X2)) |
→ |
active#(times(mark(X1),mark(X2))) |
(125) |
mark#(times(X1,X2)) |
→ |
mark#(X1) |
(127) |
mark#(times(X1,X2)) |
→ |
mark#(X2) |
(128) |
mark#(square(X)) |
→ |
active#(square(mark(X))) |
(129) |
mark#(square(X)) |
→ |
mark#(X) |
(131) |
1.1.1 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[2ndsneg(x1, x2)] |
= |
2 |
[active#(x1)] |
= |
-1 + x1
|
[2ndspos(x1, x2)] |
= |
2 |
[cons(x1, x2)] |
= |
0 |
[from(x1)] |
= |
2 |
[negrecip(x1)] |
= |
-2 |
[pi(x1)] |
= |
2 |
[plus(x1, x2)] |
= |
2 |
[posrecip(x1)] |
= |
1 |
[rcons(x1, x2)] |
= |
-2 |
[s(x1)] |
= |
-2 |
[square(x1)] |
= |
2 |
[times(x1, x2)] |
= |
2 |
[mark(x1)] |
= |
-2 |
[active(x1)] |
= |
-2 + 2 · x1
|
[0] |
= |
2 |
[rnil] |
= |
2 |
[mark#(x1)] |
= |
1 |
together with the usable
rules
from(active(X)) |
→ |
from(X) |
(27) |
from(mark(X)) |
→ |
from(X) |
(26) |
s(active(X)) |
→ |
s(X) |
(33) |
s(mark(X)) |
→ |
s(X) |
(32) |
cons(X1,mark(X2)) |
→ |
cons(X1,X2) |
(29) |
cons(mark(X1),X2) |
→ |
cons(X1,X2) |
(28) |
cons(active(X1),X2) |
→ |
cons(X1,X2) |
(30) |
cons(X1,active(X2)) |
→ |
cons(X1,X2) |
(31) |
posrecip(active(X)) |
→ |
posrecip(X) |
(43) |
posrecip(mark(X)) |
→ |
posrecip(X) |
(42) |
2ndsneg(X1,mark(X2)) |
→ |
2ndsneg(X1,X2) |
(45) |
2ndsneg(mark(X1),X2) |
→ |
2ndsneg(X1,X2) |
(44) |
2ndsneg(active(X1),X2) |
→ |
2ndsneg(X1,X2) |
(46) |
2ndsneg(X1,active(X2)) |
→ |
2ndsneg(X1,X2) |
(47) |
rcons(X1,mark(X2)) |
→ |
rcons(X1,X2) |
(39) |
rcons(mark(X1),X2) |
→ |
rcons(X1,X2) |
(38) |
rcons(active(X1),X2) |
→ |
rcons(X1,X2) |
(40) |
rcons(X1,active(X2)) |
→ |
rcons(X1,X2) |
(41) |
negrecip(active(X)) |
→ |
negrecip(X) |
(49) |
negrecip(mark(X)) |
→ |
negrecip(X) |
(48) |
2ndspos(X1,mark(X2)) |
→ |
2ndspos(X1,X2) |
(35) |
2ndspos(mark(X1),X2) |
→ |
2ndspos(X1,X2) |
(34) |
2ndspos(active(X1),X2) |
→ |
2ndspos(X1,X2) |
(36) |
2ndspos(X1,active(X2)) |
→ |
2ndspos(X1,X2) |
(37) |
plus(X1,mark(X2)) |
→ |
plus(X1,X2) |
(53) |
plus(mark(X1),X2) |
→ |
plus(X1,X2) |
(52) |
plus(active(X1),X2) |
→ |
plus(X1,X2) |
(54) |
plus(X1,active(X2)) |
→ |
plus(X1,X2) |
(55) |
times(X1,mark(X2)) |
→ |
times(X1,X2) |
(57) |
times(mark(X1),X2) |
→ |
times(X1,X2) |
(56) |
times(active(X1),X2) |
→ |
times(X1,X2) |
(58) |
times(X1,active(X2)) |
→ |
times(X1,X2) |
(59) |
pi(active(X)) |
→ |
pi(X) |
(51) |
pi(mark(X)) |
→ |
pi(X) |
(50) |
square(active(X)) |
→ |
square(X) |
(61) |
square(mark(X)) |
→ |
square(X) |
(60) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
mark#(cons(X1,X2)) |
→ |
active#(cons(mark(X1),X2)) |
(92) |
mark#(s(X)) |
→ |
active#(s(mark(X))) |
(95) |
mark#(rcons(X1,X2)) |
→ |
active#(rcons(mark(X1),mark(X2))) |
(104) |
mark#(posrecip(X)) |
→ |
active#(posrecip(mark(X))) |
(108) |
mark#(negrecip(X)) |
→ |
active#(negrecip(mark(X))) |
(115) |
could be deleted.
1.1.1.1 Reduction Pair Processor
Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals
[mark#(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[active#(x1)] |
= |
+ · x1
|
[mark(x1)] |
= |
+ · x1
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[s(x1)] |
= |
+ · x1
|
[2ndspos(x1, x2)] |
= |
+ · x1 + · x2
|
[rcons(x1, x2)] |
= |
+ · x1 + · x2
|
[posrecip(x1)] |
= |
+ · x1
|
[2ndsneg(x1, x2)] |
= |
+ · x1 + · x2
|
[negrecip(x1)] |
= |
+ · x1
|
[pi(x1)] |
= |
+ · x1
|
[0] |
= |
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[square(x1)] |
= |
+ · x1
|
[active(x1)] |
= |
+ · x1
|
[rnil] |
= |
|
the
pair
mark#(rcons(X1,X2)) |
→ |
mark#(X1) |
(106) |
could be deleted.
1.1.1.1.1 Reduction Pair Processor
Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals
[mark#(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[active#(x1)] |
= |
+ · x1
|
[mark(x1)] |
= |
+ · x1
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[s(x1)] |
= |
+ · x1
|
[2ndspos(x1, x2)] |
= |
+ · x1 + · x2
|
[rcons(x1, x2)] |
= |
+ · x1 + · x2
|
[posrecip(x1)] |
= |
+ · x1
|
[2ndsneg(x1, x2)] |
= |
+ · x1 + · x2
|
[negrecip(x1)] |
= |
+ · x1
|
[pi(x1)] |
= |
+ · x1
|
[0] |
= |
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[square(x1)] |
= |
+ · x1
|
[active(x1)] |
= |
+ · x1
|
[rnil] |
= |
|
the
pair
mark#(posrecip(X)) |
→ |
mark#(X) |
(110) |
could be deleted.
1.1.1.1.1.1 Reduction Pair Processor
Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals
[mark#(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[active#(x1)] |
= |
+ · x1
|
[mark(x1)] |
= |
+ · x1
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[s(x1)] |
= |
+ · x1
|
[2ndspos(x1, x2)] |
= |
+ · x1 + · x2
|
[rcons(x1, x2)] |
= |
+ · x1 + · x2
|
[posrecip(x1)] |
= |
+ · x1
|
[2ndsneg(x1, x2)] |
= |
+ · x1 + · x2
|
[negrecip(x1)] |
= |
+ · x1
|
[pi(x1)] |
= |
+ · x1
|
[0] |
= |
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[square(x1)] |
= |
+ · x1
|
[active(x1)] |
= |
+ · x1
|
[rnil] |
= |
|
the
pair
mark#(negrecip(X)) |
→ |
mark#(X) |
(117) |
could be deleted.
1.1.1.1.1.1.1 Reduction Pair Processor
Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals
[mark#(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[active#(x1)] |
= |
+ · x1
|
[mark(x1)] |
= |
+ · x1
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[s(x1)] |
= |
+ · x1
|
[2ndspos(x1, x2)] |
= |
+ · x1 + · x2
|
[rcons(x1, x2)] |
= |
+ · x1 + · x2
|
[posrecip(x1)] |
= |
+ · x1
|
[2ndsneg(x1, x2)] |
= |
+ · x1 + · x2
|
[negrecip(x1)] |
= |
+ · x1
|
[pi(x1)] |
= |
+ · x1
|
[0] |
= |
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[square(x1)] |
= |
+ · x1
|
[active(x1)] |
= |
+ · x1
|
[rnil] |
= |
|
the
pair
mark#(square(X)) |
→ |
mark#(X) |
(131) |
could be deleted.
1.1.1.1.1.1.1.1 Reduction Pair Processor
Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals
[mark#(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[active#(x1)] |
= |
+ · x1
|
[mark(x1)] |
= |
+ · x1
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[s(x1)] |
= |
+ · x1
|
[2ndspos(x1, x2)] |
= |
+ · x1 + · x2
|
[rcons(x1, x2)] |
= |
+ · x1 + · x2
|
[posrecip(x1)] |
= |
+ · x1
|
[2ndsneg(x1, x2)] |
= |
+ · x1 + · x2
|
[negrecip(x1)] |
= |
+ · x1
|
[pi(x1)] |
= |
+ · x1
|
[0] |
= |
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[square(x1)] |
= |
+ · x1
|
[active(x1)] |
= |
+ · x1
|
[rnil] |
= |
|
the
pair
mark#(pi(X)) |
→ |
mark#(X) |
(120) |
could be deleted.
1.1.1.1.1.1.1.1.1 Reduction Pair Processor
Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals
[mark#(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[active#(x1)] |
= |
+ · x1
|
[mark(x1)] |
= |
+ · x1
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[s(x1)] |
= |
+ · x1
|
[2ndspos(x1, x2)] |
= |
+ · x1 + · x2
|
[rcons(x1, x2)] |
= |
+ · x1 + · x2
|
[posrecip(x1)] |
= |
+ · x1
|
[2ndsneg(x1, x2)] |
= |
+ · x1 + · x2
|
[negrecip(x1)] |
= |
+ · x1
|
[pi(x1)] |
= |
+ · x1
|
[0] |
= |
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[square(x1)] |
= |
+ · x1
|
[active(x1)] |
= |
+ · x1
|
[rnil] |
= |
|
the
pair
active#(square(X)) |
→ |
mark#(times(X,X)) |
(87) |
could be deleted.
1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[2ndsneg(x1, x2)] |
= |
2 |
[active#(x1)] |
= |
-1 + x1
|
[2ndspos(x1, x2)] |
= |
2 |
[from(x1)] |
= |
2 |
[pi(x1)] |
= |
2 |
[plus(x1, x2)] |
= |
2 |
[square(x1)] |
= |
0 |
[times(x1, x2)] |
= |
2 |
[mark(x1)] |
= |
1 |
[active(x1)] |
= |
-2 |
[cons(x1, x2)] |
= |
-2 + x1
|
[s(x1)] |
= |
-2 + 2 · x1
|
[rcons(x1, x2)] |
= |
-2 + 2 · x1
|
[posrecip(x1)] |
= |
1 + x1
|
[negrecip(x1)] |
= |
1 + x1
|
[0] |
= |
0 |
[rnil] |
= |
0 |
[mark#(x1)] |
= |
1 |
together with the usable
rules
from(active(X)) |
→ |
from(X) |
(27) |
from(mark(X)) |
→ |
from(X) |
(26) |
2ndsneg(X1,mark(X2)) |
→ |
2ndsneg(X1,X2) |
(45) |
2ndsneg(mark(X1),X2) |
→ |
2ndsneg(X1,X2) |
(44) |
2ndsneg(active(X1),X2) |
→ |
2ndsneg(X1,X2) |
(46) |
2ndsneg(X1,active(X2)) |
→ |
2ndsneg(X1,X2) |
(47) |
2ndspos(X1,mark(X2)) |
→ |
2ndspos(X1,X2) |
(35) |
2ndspos(mark(X1),X2) |
→ |
2ndspos(X1,X2) |
(34) |
2ndspos(active(X1),X2) |
→ |
2ndspos(X1,X2) |
(36) |
2ndspos(X1,active(X2)) |
→ |
2ndspos(X1,X2) |
(37) |
plus(X1,mark(X2)) |
→ |
plus(X1,X2) |
(53) |
plus(mark(X1),X2) |
→ |
plus(X1,X2) |
(52) |
plus(active(X1),X2) |
→ |
plus(X1,X2) |
(54) |
plus(X1,active(X2)) |
→ |
plus(X1,X2) |
(55) |
times(X1,mark(X2)) |
→ |
times(X1,X2) |
(57) |
times(mark(X1),X2) |
→ |
times(X1,X2) |
(56) |
times(active(X1),X2) |
→ |
times(X1,X2) |
(58) |
times(X1,active(X2)) |
→ |
times(X1,X2) |
(59) |
pi(active(X)) |
→ |
pi(X) |
(51) |
pi(mark(X)) |
→ |
pi(X) |
(50) |
square(active(X)) |
→ |
square(X) |
(61) |
square(mark(X)) |
→ |
square(X) |
(60) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
mark#(square(X)) |
→ |
active#(square(mark(X))) |
(129) |
could be deleted.
1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor
Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals
[mark#(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[active#(x1)] |
= |
+ · x1
|
[mark(x1)] |
= |
+ · x1
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[s(x1)] |
= |
+ · x1
|
[2ndspos(x1, x2)] |
= |
+ · x1 + · x2
|
[rcons(x1, x2)] |
= |
+ · x1 + · x2
|
[posrecip(x1)] |
= |
+ · x1
|
[2ndsneg(x1, x2)] |
= |
+ · x1 + · x2
|
[negrecip(x1)] |
= |
+ · x1
|
[pi(x1)] |
= |
+ · x1
|
[0] |
= |
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[active(x1)] |
= |
+ · x1
|
[square(x1)] |
= |
+ · x1
|
[rnil] |
= |
|
the
pair
mark#(from(X)) |
→ |
mark#(X) |
(91) |
could be deleted.
1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor
Using the matrix interpretations of dimension 1 with strict dimension 1 over the arctic semiring over the naturals
[mark#(x1)] |
= |
+ · x1
|
[from(x1)] |
= |
+ · x1
|
[active#(x1)] |
= |
+ · x1
|
[mark(x1)] |
= |
+ · x1
|
[cons(x1, x2)] |
= |
+ · x1 + · x2
|
[s(x1)] |
= |
+ · x1
|
[2ndspos(x1, x2)] |
= |
+ · x1 + · x2
|
[rcons(x1, x2)] |
= |
+ · x1 + · x2
|
[posrecip(x1)] |
= |
+ · x1
|
[2ndsneg(x1, x2)] |
= |
+ · x1 + · x2
|
[negrecip(x1)] |
= |
+ · x1
|
[pi(x1)] |
= |
+ · x1
|
[0] |
= |
|
[plus(x1, x2)] |
= |
+ · x1 + · x2
|
[times(x1, x2)] |
= |
+ · x1 + · x2
|
[active(x1)] |
= |
+ · x1
|
[square(x1)] |
= |
+ · x1
|
[rnil] |
= |
|
the
pair
mark#(cons(X1,X2)) |
→ |
mark#(X1) |
(94) |
could be deleted.
1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor
Using the
prec(from) |
= |
4 |
|
stat(from) |
= |
lex
|
prec(s) |
= |
3 |
|
stat(s) |
= |
lex
|
prec(2ndspos) |
= |
1 |
|
stat(2ndspos) |
= |
mul
|
prec(rcons) |
= |
0 |
|
stat(rcons) |
= |
lex
|
prec(posrecip) |
= |
2 |
|
stat(posrecip) |
= |
mul
|
prec(2ndsneg) |
= |
1 |
|
stat(2ndsneg) |
= |
mul
|
prec(negrecip) |
= |
3 |
|
stat(negrecip) |
= |
lex
|
prec(pi) |
= |
7 |
|
stat(pi) |
= |
lex
|
prec(0) |
= |
6 |
|
stat(0) |
= |
mul
|
prec(plus) |
= |
8 |
|
stat(plus) |
= |
mul
|
prec(times) |
= |
9 |
|
stat(times) |
= |
lex
|
prec(square) |
= |
10 |
|
stat(square) |
= |
lex
|
prec(rnil) |
= |
5 |
|
stat(rnil) |
= |
mul
|
π(mark#) |
= |
1 |
π(from) |
= |
[] |
π(active#) |
= |
1 |
π(mark) |
= |
1 |
π(cons) |
= |
2 |
π(s) |
= |
[1] |
π(2ndspos) |
= |
[1,2] |
π(rcons) |
= |
[1,2] |
π(posrecip) |
= |
[] |
π(2ndsneg) |
= |
[1,2] |
π(negrecip) |
= |
[] |
π(pi) |
= |
[1] |
π(0) |
= |
[] |
π(plus) |
= |
[1,2] |
π(times) |
= |
[1,2] |
π(active) |
= |
1 |
π(square) |
= |
[1] |
π(rnil) |
= |
[] |
the
pairs
active#(2ndspos(s(N),cons(X,cons(Y,Z)))) |
→ |
mark#(rcons(posrecip(Y),2ndsneg(N,Z))) |
(67) |
active#(2ndsneg(s(N),cons(X,cons(Y,Z)))) |
→ |
mark#(rcons(negrecip(Y),2ndspos(N,Z))) |
(72) |
mark#(s(X)) |
→ |
mark#(X) |
(97) |
active#(pi(X)) |
→ |
mark#(2ndspos(X,from(0))) |
(76) |
mark#(2ndspos(X1,X2)) |
→ |
mark#(X1) |
(100) |
mark#(2ndspos(X1,X2)) |
→ |
mark#(X2) |
(101) |
active#(plus(0,Y)) |
→ |
mark#(Y) |
(79) |
mark#(rcons(X1,X2)) |
→ |
mark#(X2) |
(107) |
active#(plus(s(X),Y)) |
→ |
mark#(s(plus(X,Y))) |
(80) |
active#(times(s(X),Y)) |
→ |
mark#(plus(Y,times(X,Y))) |
(84) |
mark#(2ndsneg(X1,X2)) |
→ |
mark#(X1) |
(113) |
mark#(2ndsneg(X1,X2)) |
→ |
mark#(X2) |
(114) |
mark#(plus(X1,X2)) |
→ |
mark#(X1) |
(123) |
mark#(plus(X1,X2)) |
→ |
mark#(X2) |
(124) |
mark#(times(X1,X2)) |
→ |
mark#(X1) |
(127) |
mark#(times(X1,X2)) |
→ |
mark#(X2) |
(128) |
could be deleted.
1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules
Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(from) |
= |
6 |
|
weight(from) |
= |
2 |
|
|
|
prec(active#) |
= |
1 |
|
weight(active#) |
= |
1 |
|
|
|
prec(cons) |
= |
0 |
|
weight(cons) |
= |
1 |
|
|
|
prec(2ndspos) |
= |
3 |
|
weight(2ndspos) |
= |
2 |
|
|
|
prec(2ndsneg) |
= |
5 |
|
weight(2ndsneg) |
= |
2 |
|
|
|
prec(pi) |
= |
4 |
|
weight(pi) |
= |
2 |
|
|
|
prec(plus) |
= |
2 |
|
weight(plus) |
= |
1 |
|
|
|
prec(times) |
= |
7 |
|
weight(times) |
= |
2 |
|
|
|
in combination with the following argument filter
π(mark#) |
= |
1 |
π(from) |
= |
[] |
π(active#) |
= |
[] |
π(cons) |
= |
[] |
π(2ndspos) |
= |
[] |
π(2ndsneg) |
= |
[] |
π(pi) |
= |
[] |
π(plus) |
= |
[] |
π(times) |
= |
[] |
together with the usable
rules
cons(X1,mark(X2)) |
→ |
cons(X1,X2) |
(29) |
cons(mark(X1),X2) |
→ |
cons(X1,X2) |
(28) |
cons(active(X1),X2) |
→ |
cons(X1,X2) |
(30) |
cons(X1,active(X2)) |
→ |
cons(X1,X2) |
(31) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
mark#(from(X)) |
→ |
active#(from(mark(X))) |
(89) |
active#(from(X)) |
→ |
mark#(cons(X,from(s(X)))) |
(62) |
mark#(2ndspos(X1,X2)) |
→ |
active#(2ndspos(mark(X1),mark(X2))) |
(98) |
mark#(2ndsneg(X1,X2)) |
→ |
active#(2ndsneg(mark(X1),mark(X2))) |
(111) |
mark#(pi(X)) |
→ |
active#(pi(mark(X))) |
(118) |
mark#(plus(X1,X2)) |
→ |
active#(plus(mark(X1),mark(X2))) |
(121) |
mark#(times(X1,X2)) |
→ |
active#(times(mark(X1),mark(X2))) |
(125) |
could be deleted.
1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 P is empty
There are no pairs anymore.
-
The
2nd
component contains the
pair
from#(active(X)) |
→ |
from#(X) |
(133) |
from#(mark(X)) |
→ |
from#(X) |
(132) |
1.1.2 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[active(x1)] |
= |
1 · x1
|
[mark(x1)] |
= |
1 · x1
|
[from#(x1)] |
= |
1 · x1
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
rule
could be deleted.
1.1.2.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
from#(active(X)) |
→ |
from#(X) |
(133) |
|
1 |
> |
1 |
from#(mark(X)) |
→ |
from#(X) |
(132) |
|
1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
3rd
component contains the
pair
cons#(X1,mark(X2)) |
→ |
cons#(X1,X2) |
(135) |
cons#(mark(X1),X2) |
→ |
cons#(X1,X2) |
(134) |
cons#(active(X1),X2) |
→ |
cons#(X1,X2) |
(136) |
cons#(X1,active(X2)) |
→ |
cons#(X1,X2) |
(137) |
1.1.3 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[mark(x1)] |
= |
1 · x1
|
[active(x1)] |
= |
1 · x1
|
[cons#(x1, x2)] |
= |
1 · x1 + 1 · x2
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
rule
could be deleted.
1.1.3.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
cons#(X1,mark(X2)) |
→ |
cons#(X1,X2) |
(135) |
|
1 |
≥ |
1 |
2 |
> |
2 |
cons#(mark(X1),X2) |
→ |
cons#(X1,X2) |
(134) |
|
1 |
> |
1 |
2 |
≥ |
2 |
cons#(active(X1),X2) |
→ |
cons#(X1,X2) |
(136) |
|
1 |
> |
1 |
2 |
≥ |
2 |
cons#(X1,active(X2)) |
→ |
cons#(X1,X2) |
(137) |
|
1 |
≥ |
1 |
2 |
> |
2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
4th
component contains the
pair
s#(active(X)) |
→ |
s#(X) |
(139) |
s#(mark(X)) |
→ |
s#(X) |
(138) |
1.1.4 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[active(x1)] |
= |
1 · x1
|
[mark(x1)] |
= |
1 · x1
|
[s#(x1)] |
= |
1 · x1
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
rule
could be deleted.
1.1.4.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
s#(active(X)) |
→ |
s#(X) |
(139) |
|
1 |
> |
1 |
s#(mark(X)) |
→ |
s#(X) |
(138) |
|
1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
5th
component contains the
pair
2ndspos#(X1,mark(X2)) |
→ |
2ndspos#(X1,X2) |
(141) |
2ndspos#(mark(X1),X2) |
→ |
2ndspos#(X1,X2) |
(140) |
2ndspos#(active(X1),X2) |
→ |
2ndspos#(X1,X2) |
(142) |
2ndspos#(X1,active(X2)) |
→ |
2ndspos#(X1,X2) |
(143) |
1.1.5 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[mark(x1)] |
= |
1 · x1
|
[active(x1)] |
= |
1 · x1
|
[2ndspos#(x1, x2)] |
= |
1 · x1 + 1 · x2
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
rule
could be deleted.
1.1.5.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
2ndspos#(X1,mark(X2)) |
→ |
2ndspos#(X1,X2) |
(141) |
|
1 |
≥ |
1 |
2 |
> |
2 |
2ndspos#(mark(X1),X2) |
→ |
2ndspos#(X1,X2) |
(140) |
|
1 |
> |
1 |
2 |
≥ |
2 |
2ndspos#(active(X1),X2) |
→ |
2ndspos#(X1,X2) |
(142) |
|
1 |
> |
1 |
2 |
≥ |
2 |
2ndspos#(X1,active(X2)) |
→ |
2ndspos#(X1,X2) |
(143) |
|
1 |
≥ |
1 |
2 |
> |
2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
6th
component contains the
pair
rcons#(X1,mark(X2)) |
→ |
rcons#(X1,X2) |
(145) |
rcons#(mark(X1),X2) |
→ |
rcons#(X1,X2) |
(144) |
rcons#(active(X1),X2) |
→ |
rcons#(X1,X2) |
(146) |
rcons#(X1,active(X2)) |
→ |
rcons#(X1,X2) |
(147) |
1.1.6 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[mark(x1)] |
= |
1 · x1
|
[active(x1)] |
= |
1 · x1
|
[rcons#(x1, x2)] |
= |
1 · x1 + 1 · x2
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
rule
could be deleted.
1.1.6.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
rcons#(X1,mark(X2)) |
→ |
rcons#(X1,X2) |
(145) |
|
1 |
≥ |
1 |
2 |
> |
2 |
rcons#(mark(X1),X2) |
→ |
rcons#(X1,X2) |
(144) |
|
1 |
> |
1 |
2 |
≥ |
2 |
rcons#(active(X1),X2) |
→ |
rcons#(X1,X2) |
(146) |
|
1 |
> |
1 |
2 |
≥ |
2 |
rcons#(X1,active(X2)) |
→ |
rcons#(X1,X2) |
(147) |
|
1 |
≥ |
1 |
2 |
> |
2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
7th
component contains the
pair
posrecip#(active(X)) |
→ |
posrecip#(X) |
(149) |
posrecip#(mark(X)) |
→ |
posrecip#(X) |
(148) |
1.1.7 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[active(x1)] |
= |
1 · x1
|
[mark(x1)] |
= |
1 · x1
|
[posrecip#(x1)] |
= |
1 · x1
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
rule
could be deleted.
1.1.7.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
posrecip#(active(X)) |
→ |
posrecip#(X) |
(149) |
|
1 |
> |
1 |
posrecip#(mark(X)) |
→ |
posrecip#(X) |
(148) |
|
1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
8th
component contains the
pair
2ndsneg#(X1,mark(X2)) |
→ |
2ndsneg#(X1,X2) |
(151) |
2ndsneg#(mark(X1),X2) |
→ |
2ndsneg#(X1,X2) |
(150) |
2ndsneg#(active(X1),X2) |
→ |
2ndsneg#(X1,X2) |
(152) |
2ndsneg#(X1,active(X2)) |
→ |
2ndsneg#(X1,X2) |
(153) |
1.1.8 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[mark(x1)] |
= |
1 · x1
|
[active(x1)] |
= |
1 · x1
|
[2ndsneg#(x1, x2)] |
= |
1 · x1 + 1 · x2
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
rule
could be deleted.
1.1.8.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
2ndsneg#(X1,mark(X2)) |
→ |
2ndsneg#(X1,X2) |
(151) |
|
1 |
≥ |
1 |
2 |
> |
2 |
2ndsneg#(mark(X1),X2) |
→ |
2ndsneg#(X1,X2) |
(150) |
|
1 |
> |
1 |
2 |
≥ |
2 |
2ndsneg#(active(X1),X2) |
→ |
2ndsneg#(X1,X2) |
(152) |
|
1 |
> |
1 |
2 |
≥ |
2 |
2ndsneg#(X1,active(X2)) |
→ |
2ndsneg#(X1,X2) |
(153) |
|
1 |
≥ |
1 |
2 |
> |
2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
9th
component contains the
pair
negrecip#(active(X)) |
→ |
negrecip#(X) |
(155) |
negrecip#(mark(X)) |
→ |
negrecip#(X) |
(154) |
1.1.9 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[active(x1)] |
= |
1 · x1
|
[mark(x1)] |
= |
1 · x1
|
[negrecip#(x1)] |
= |
1 · x1
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
rule
could be deleted.
1.1.9.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
negrecip#(active(X)) |
→ |
negrecip#(X) |
(155) |
|
1 |
> |
1 |
negrecip#(mark(X)) |
→ |
negrecip#(X) |
(154) |
|
1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
10th
component contains the
pair
pi#(active(X)) |
→ |
pi#(X) |
(157) |
pi#(mark(X)) |
→ |
pi#(X) |
(156) |
1.1.10 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[active(x1)] |
= |
1 · x1
|
[mark(x1)] |
= |
1 · x1
|
[pi#(x1)] |
= |
1 · x1
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
rule
could be deleted.
1.1.10.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
pi#(active(X)) |
→ |
pi#(X) |
(157) |
|
1 |
> |
1 |
pi#(mark(X)) |
→ |
pi#(X) |
(156) |
|
1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
11th
component contains the
pair
plus#(X1,mark(X2)) |
→ |
plus#(X1,X2) |
(159) |
plus#(mark(X1),X2) |
→ |
plus#(X1,X2) |
(158) |
plus#(active(X1),X2) |
→ |
plus#(X1,X2) |
(160) |
plus#(X1,active(X2)) |
→ |
plus#(X1,X2) |
(161) |
1.1.11 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[mark(x1)] |
= |
1 · x1
|
[active(x1)] |
= |
1 · x1
|
[plus#(x1, x2)] |
= |
1 · x1 + 1 · x2
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
rule
could be deleted.
1.1.11.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
plus#(X1,mark(X2)) |
→ |
plus#(X1,X2) |
(159) |
|
1 |
≥ |
1 |
2 |
> |
2 |
plus#(mark(X1),X2) |
→ |
plus#(X1,X2) |
(158) |
|
1 |
> |
1 |
2 |
≥ |
2 |
plus#(active(X1),X2) |
→ |
plus#(X1,X2) |
(160) |
|
1 |
> |
1 |
2 |
≥ |
2 |
plus#(X1,active(X2)) |
→ |
plus#(X1,X2) |
(161) |
|
1 |
≥ |
1 |
2 |
> |
2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
12th
component contains the
pair
times#(X1,mark(X2)) |
→ |
times#(X1,X2) |
(163) |
times#(mark(X1),X2) |
→ |
times#(X1,X2) |
(162) |
times#(active(X1),X2) |
→ |
times#(X1,X2) |
(164) |
times#(X1,active(X2)) |
→ |
times#(X1,X2) |
(165) |
1.1.12 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[mark(x1)] |
= |
1 · x1
|
[active(x1)] |
= |
1 · x1
|
[times#(x1, x2)] |
= |
1 · x1 + 1 · x2
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
rule
could be deleted.
1.1.12.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
times#(X1,mark(X2)) |
→ |
times#(X1,X2) |
(163) |
|
1 |
≥ |
1 |
2 |
> |
2 |
times#(mark(X1),X2) |
→ |
times#(X1,X2) |
(162) |
|
1 |
> |
1 |
2 |
≥ |
2 |
times#(active(X1),X2) |
→ |
times#(X1,X2) |
(164) |
|
1 |
> |
1 |
2 |
≥ |
2 |
times#(X1,active(X2)) |
→ |
times#(X1,X2) |
(165) |
|
1 |
≥ |
1 |
2 |
> |
2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
13th
component contains the
pair
square#(active(X)) |
→ |
square#(X) |
(167) |
square#(mark(X)) |
→ |
square#(X) |
(166) |
1.1.13 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[active(x1)] |
= |
1 · x1
|
[mark(x1)] |
= |
1 · x1
|
[square#(x1)] |
= |
1 · x1
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
rule
could be deleted.
1.1.13.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
square#(active(X)) |
→ |
square#(X) |
(167) |
|
1 |
> |
1 |
square#(mark(X)) |
→ |
square#(X) |
(166) |
|
1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.