The
1st
component contains the
pair
top#(mark(f(x0,x1))) |
→ |
top#(f(proper(x0),proper(x1))) |
(26) |
top#(ok(f(x0,x0))) |
→ |
top#(mark(f(a,b))) |
(23) |
top#(ok(f(x0,x1))) |
→ |
top#(f(active(x0),x1)) |
(25) |
1.1.1.1.1.1.1 Split
We split (P,R) into the relative DP-problem (PD,P-PD,RD,R-RD) and (P-PD,R-RD) where the pairs PD
top#(ok(f(x0,x0))) |
→ |
top#(mark(f(a,b))) |
(23) |
and the rules RD
There are no rules.
are deleted.
1.1.1.1.1.1.1.1 Semantic Labeling Processor
The following interpretations form a
model
of the rules.
As carrier we take the set
{0,1}.
Symbols are labeled by the interpretation of their arguments using the interpretations
(modulo 2):
[active(x1)] |
= |
0 |
[a] |
= |
1 |
[b] |
= |
0 |
[proper(x1)] |
= |
0 |
[f(x1, x2)] |
= |
0 |
[top#(x1)] |
= |
0 |
[ok(x1)] |
= |
0 |
[mark(x1)] |
= |
0 |
We obtain the set of labeled pairs
top#0(mark0(f00(x0,x1))) |
→ |
top#0(f00(proper0(x0),proper0(x1))) |
(29) |
top#0(ok0(f00(x0,x0))) |
→ |
top#0(mark0(f10(a,b))) |
(30) |
top#0(ok0(f11(x0,x0))) |
→ |
top#0(mark0(f10(a,b))) |
(31) |
top#0(mark0(f01(x0,x1))) |
→ |
top#0(f00(proper0(x0),proper1(x1))) |
(32) |
top#0(mark0(f10(x0,x1))) |
→ |
top#0(f00(proper1(x0),proper0(x1))) |
(33) |
top#0(mark0(f11(x0,x1))) |
→ |
top#0(f00(proper1(x0),proper1(x1))) |
(34) |
top#0(ok0(f00(x0,x1))) |
→ |
top#0(f00(active0(x0),x1)) |
(35) |
top#0(ok0(f01(x0,x1))) |
→ |
top#0(f01(active0(x0),x1)) |
(36) |
top#0(ok0(f10(x0,x1))) |
→ |
top#0(f00(active1(x0),x1)) |
(37) |
top#0(ok0(f11(x0,x1))) |
→ |
top#0(f01(active1(x0),x1)) |
(38) |
and the set of labeled rules:
proper0(f00(X1,X2)) |
→ |
f00(proper0(X1),proper0(X2)) |
(39) |
proper0(f01(X1,X2)) |
→ |
f00(proper0(X1),proper1(X2)) |
(40) |
proper0(f10(X1,X2)) |
→ |
f00(proper1(X1),proper0(X2)) |
(41) |
proper0(f11(X1,X2)) |
→ |
f00(proper1(X1),proper1(X2)) |
(42) |
proper1(a) |
→ |
ok1(a) |
(43) |
proper0(b) |
→ |
ok0(b) |
(44) |
f00(mark0(X1),X2) |
→ |
mark0(f00(X1,X2)) |
(45) |
f01(mark0(X1),X2) |
→ |
mark0(f01(X1,X2)) |
(46) |
f00(mark1(X1),X2) |
→ |
mark0(f10(X1,X2)) |
(47) |
f01(mark1(X1),X2) |
→ |
mark0(f11(X1,X2)) |
(48) |
f00(ok0(X1),ok0(X2)) |
→ |
ok0(f00(X1,X2)) |
(49) |
f00(ok0(X1),ok1(X2)) |
→ |
ok0(f01(X1,X2)) |
(50) |
f00(ok1(X1),ok0(X2)) |
→ |
ok0(f10(X1,X2)) |
(51) |
f00(ok1(X1),ok1(X2)) |
→ |
ok0(f11(X1,X2)) |
(52) |
active0(f00(X,X)) |
→ |
mark0(f10(a,b)) |
(53) |
active0(f11(X,X)) |
→ |
mark0(f10(a,b)) |
(54) |
active0(b) |
→ |
mark1(a) |
(55) |
active0(f00(X1,X2)) |
→ |
f00(active0(X1),X2) |
(56) |
active0(f01(X1,X2)) |
→ |
f01(active0(X1),X2) |
(57) |
active0(f10(X1,X2)) |
→ |
f00(active1(X1),X2) |
(58) |
active0(f11(X1,X2)) |
→ |
f01(active1(X1),X2) |
(59) |
1.1.1.1.1.1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
1.1.1.1.1.1.1.2 Split
We split (P,R) into the relative DP-problem (PD,P-PD,RD,R-RD) and (P-PD,R-RD) where the pairs PD
There are no rules.
and the rules RD
are deleted.
1.1.1.1.1.1.1.2.1 Semantic Labeling Processor
The following interpretations form a
model
of the rules.
As carrier we take the set
{0,1}.
Symbols are labeled by the interpretation of their arguments using the interpretations
(modulo 2):
[active(x1)] |
= |
0 |
[a] |
= |
0 |
[b] |
= |
1 |
[proper(x1)] |
= |
0 |
[f(x1, x2)] |
= |
1x1
|
[top#(x1)] |
= |
0 |
[ok(x1)] |
= |
0 |
[mark(x1)] |
= |
0 |
We obtain the set of labeled pairs
top#0(mark0(f00(x0,x1))) |
→ |
top#0(f00(proper0(x0),proper0(x1))) |
(29) |
top#0(ok0(f00(x0,x1))) |
→ |
top#0(f00(active0(x0),x1)) |
(35) |
top#0(ok0(f01(x0,x1))) |
→ |
top#0(f01(active0(x0),x1)) |
(36) |
top#0(ok1(f10(x0,x1))) |
→ |
top#0(f00(active1(x0),x1)) |
(60) |
top#0(ok1(f11(x0,x1))) |
→ |
top#0(f01(active1(x0),x1)) |
(61) |
top#0(mark0(f01(x0,x1))) |
→ |
top#0(f00(proper0(x0),proper1(x1))) |
(32) |
top#0(mark1(f10(x0,x1))) |
→ |
top#0(f00(proper1(x0),proper0(x1))) |
(62) |
top#0(mark1(f11(x0,x1))) |
→ |
top#0(f00(proper1(x0),proper1(x1))) |
(63) |
and the set of labeled rules:
proper0(f00(X1,X2)) |
→ |
f00(proper0(X1),proper0(X2)) |
(39) |
proper0(f01(X1,X2)) |
→ |
f00(proper0(X1),proper1(X2)) |
(40) |
proper1(f10(X1,X2)) |
→ |
f00(proper1(X1),proper0(X2)) |
(64) |
proper1(f11(X1,X2)) |
→ |
f00(proper1(X1),proper1(X2)) |
(65) |
proper0(a) |
→ |
ok0(a) |
(66) |
proper1(b) |
→ |
ok1(b) |
(67) |
f00(mark0(X1),X2) |
→ |
mark0(f00(X1,X2)) |
(45) |
f01(mark0(X1),X2) |
→ |
mark0(f01(X1,X2)) |
(46) |
f00(mark1(X1),X2) |
→ |
mark1(f10(X1,X2)) |
(68) |
f01(mark1(X1),X2) |
→ |
mark1(f11(X1,X2)) |
(69) |
f00(ok0(X1),ok0(X2)) |
→ |
ok0(f00(X1,X2)) |
(49) |
f00(ok0(X1),ok1(X2)) |
→ |
ok0(f01(X1,X2)) |
(50) |
f00(ok1(X1),ok0(X2)) |
→ |
ok1(f10(X1,X2)) |
(70) |
f00(ok1(X1),ok1(X2)) |
→ |
ok1(f11(X1,X2)) |
(71) |
active0(f00(X,X)) |
→ |
mark0(f01(a,b)) |
(72) |
active1(f11(X,X)) |
→ |
mark0(f01(a,b)) |
(73) |
active1(b) |
→ |
mark0(a) |
(74) |
active0(f00(X1,X2)) |
→ |
f00(active0(X1),X2) |
(56) |
active0(f01(X1,X2)) |
→ |
f01(active0(X1),X2) |
(57) |
active1(f10(X1,X2)) |
→ |
f00(active1(X1),X2) |
(75) |
active1(f11(X1,X2)) |
→ |
f01(active1(X1),X2) |
(76) |
1.1.1.1.1.1.1.2.1.1 Monotonic Reduction Pair Processor
Using the linear polynomial interpretation over the naturals
[proper0(x1)] |
= |
1 · x1
|
[f00(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[f01(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[proper1(x1)] |
= |
1 · x1
|
[f10(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[f11(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[a] |
= |
0 |
[ok0(x1)] |
= |
1 · x1
|
[b] |
= |
0 |
[ok1(x1)] |
= |
1 · x1
|
[mark0(x1)] |
= |
1 · x1
|
[mark1(x1)] |
= |
1 + 1 · x1
|
[active0(x1)] |
= |
1 · x1
|
[active1(x1)] |
= |
1 · x1
|
[top#0(x1)] |
= |
1 · x1
|
the
pairs
top#0(mark1(f10(x0,x1))) |
→ |
top#0(f00(proper1(x0),proper0(x1))) |
(62) |
top#0(mark1(f11(x0,x1))) |
→ |
top#0(f00(proper1(x0),proper1(x1))) |
(63) |
and
no rules
could be deleted.
1.1.1.1.1.1.1.2.1.1.1 Reduction Pair Processor
Using the linear polynomial interpretation over the naturals
[top#0(x1)] |
= |
1 · x1
|
[mark0(x1)] |
= |
0 |
[f00(x1, x2)] |
= |
1 · x1
|
[proper0(x1)] |
= |
0 |
[ok0(x1)] |
= |
0 |
[active0(x1)] |
= |
0 |
[f01(x1, x2)] |
= |
0 |
[ok1(x1)] |
= |
1 |
[f10(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[active1(x1)] |
= |
0 |
[f11(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[proper1(x1)] |
= |
1 · x1
|
[a] |
= |
0 |
[mark1(x1)] |
= |
0 |
[b] |
= |
1 |
the
pairs
top#0(ok1(f10(x0,x1))) |
→ |
top#0(f00(active1(x0),x1)) |
(60) |
top#0(ok1(f11(x0,x1))) |
→ |
top#0(f01(active1(x0),x1)) |
(61) |
could be deleted.
1.1.1.1.1.1.1.2.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[proper0(x1)] |
= |
1 · x1
|
[f00(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[f01(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[proper1(x1)] |
= |
1 · x1
|
[a] |
= |
0 |
[ok0(x1)] |
= |
1 · x1
|
[f10(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[f11(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[b] |
= |
0 |
[ok1(x1)] |
= |
1 · x1
|
[mark0(x1)] |
= |
1 · x1
|
[mark1(x1)] |
= |
1 · x1
|
[active0(x1)] |
= |
1 · x1
|
[top#0(x1)] |
= |
1 · x1
|
together with the usable
rules
proper0(f00(X1,X2)) |
→ |
f00(proper0(X1),proper0(X2)) |
(39) |
proper0(f01(X1,X2)) |
→ |
f00(proper0(X1),proper1(X2)) |
(40) |
proper0(a) |
→ |
ok0(a) |
(66) |
proper1(f10(X1,X2)) |
→ |
f00(proper1(X1),proper0(X2)) |
(64) |
proper1(f11(X1,X2)) |
→ |
f00(proper1(X1),proper1(X2)) |
(65) |
proper1(b) |
→ |
ok1(b) |
(67) |
f00(mark0(X1),X2) |
→ |
mark0(f00(X1,X2)) |
(45) |
f00(mark1(X1),X2) |
→ |
mark1(f10(X1,X2)) |
(68) |
f00(ok0(X1),ok0(X2)) |
→ |
ok0(f00(X1,X2)) |
(49) |
f00(ok0(X1),ok1(X2)) |
→ |
ok0(f01(X1,X2)) |
(50) |
f00(ok1(X1),ok0(X2)) |
→ |
ok1(f10(X1,X2)) |
(70) |
f00(ok1(X1),ok1(X2)) |
→ |
ok1(f11(X1,X2)) |
(71) |
f01(mark0(X1),X2) |
→ |
mark0(f01(X1,X2)) |
(46) |
f01(mark1(X1),X2) |
→ |
mark1(f11(X1,X2)) |
(69) |
active0(f00(X,X)) |
→ |
mark0(f01(a,b)) |
(72) |
active0(f00(X1,X2)) |
→ |
f00(active0(X1),X2) |
(56) |
active0(f01(X1,X2)) |
→ |
f01(active0(X1),X2) |
(57) |
(w.r.t. the implicit argument filter of the reduction pair),
the
rule
could be deleted.
1.1.1.1.1.1.1.2.1.1.1.1.1 P is empty
There are no pairs anymore.
1.1.1.1.1.1.1.2.2 Semantic Labeling Processor
The following interpretations form a
model
of the rules.
As carrier we take the set
{0,1}.
Symbols are labeled by the interpretation of their arguments using the interpretations
(modulo 2):
[active(x1)] |
= |
0 |
[a] |
= |
1 |
[b] |
= |
0 |
[proper(x1)] |
= |
0 |
[f(x1, x2)] |
= |
1x1
|
[top#(x1)] |
= |
0 |
[ok(x1)] |
= |
0 |
[mark(x1)] |
= |
0 |
We obtain the set of labeled pairs
top#0(mark0(f00(x0,x1))) |
→ |
top#0(f00(proper0(x0),proper0(x1))) |
(29) |
top#0(ok0(f00(x0,x1))) |
→ |
top#0(f00(active0(x0),x1)) |
(35) |
top#0(ok0(f01(x0,x1))) |
→ |
top#0(f01(active0(x0),x1)) |
(36) |
top#0(ok1(f10(x0,x1))) |
→ |
top#0(f00(active1(x0),x1)) |
(60) |
top#0(ok1(f11(x0,x1))) |
→ |
top#0(f01(active1(x0),x1)) |
(61) |
top#0(mark0(f01(x0,x1))) |
→ |
top#0(f00(proper0(x0),proper1(x1))) |
(32) |
top#0(mark1(f10(x0,x1))) |
→ |
top#0(f00(proper1(x0),proper0(x1))) |
(62) |
top#0(mark1(f11(x0,x1))) |
→ |
top#0(f00(proper1(x0),proper1(x1))) |
(63) |
and the set of labeled rules:
proper0(f00(X1,X2)) |
→ |
f00(proper0(X1),proper0(X2)) |
(39) |
proper0(f01(X1,X2)) |
→ |
f00(proper0(X1),proper1(X2)) |
(40) |
proper1(f10(X1,X2)) |
→ |
f00(proper1(X1),proper0(X2)) |
(64) |
proper1(f11(X1,X2)) |
→ |
f00(proper1(X1),proper1(X2)) |
(65) |
proper1(a) |
→ |
ok1(a) |
(43) |
proper0(b) |
→ |
ok0(b) |
(44) |
f00(mark0(X1),X2) |
→ |
mark0(f00(X1,X2)) |
(45) |
f01(mark0(X1),X2) |
→ |
mark0(f01(X1,X2)) |
(46) |
f00(mark1(X1),X2) |
→ |
mark1(f10(X1,X2)) |
(68) |
f01(mark1(X1),X2) |
→ |
mark1(f11(X1,X2)) |
(69) |
f00(ok0(X1),ok0(X2)) |
→ |
ok0(f00(X1,X2)) |
(49) |
f00(ok0(X1),ok1(X2)) |
→ |
ok0(f01(X1,X2)) |
(50) |
f00(ok1(X1),ok0(X2)) |
→ |
ok1(f10(X1,X2)) |
(70) |
f00(ok1(X1),ok1(X2)) |
→ |
ok1(f11(X1,X2)) |
(71) |
active0(f00(X,X)) |
→ |
mark1(f10(a,b)) |
(77) |
active1(f11(X,X)) |
→ |
mark1(f10(a,b)) |
(78) |
active0(f00(X1,X2)) |
→ |
f00(active0(X1),X2) |
(56) |
active0(f01(X1,X2)) |
→ |
f01(active0(X1),X2) |
(57) |
active1(f10(X1,X2)) |
→ |
f00(active1(X1),X2) |
(75) |
active1(f11(X1,X2)) |
→ |
f01(active1(X1),X2) |
(76) |
1.1.1.1.1.1.1.2.2.1 Monotonic Reduction Pair Processor
Using the linear polynomial interpretation over the naturals
[proper0(x1)] |
= |
1 · x1
|
[f00(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[f01(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[proper1(x1)] |
= |
1 · x1
|
[f10(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[f11(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[a] |
= |
0 |
[ok1(x1)] |
= |
1 · x1
|
[b] |
= |
0 |
[ok0(x1)] |
= |
1 · x1
|
[mark0(x1)] |
= |
1 + 1 · x1
|
[mark1(x1)] |
= |
1 · x1
|
[active0(x1)] |
= |
1 · x1
|
[active1(x1)] |
= |
1 · x1
|
[top#0(x1)] |
= |
1 · x1
|
the
pairs
top#0(mark0(f00(x0,x1))) |
→ |
top#0(f00(proper0(x0),proper0(x1))) |
(29) |
top#0(mark0(f01(x0,x1))) |
→ |
top#0(f00(proper0(x0),proper1(x1))) |
(32) |
and
no rules
could be deleted.
1.1.1.1.1.1.1.2.2.1.1 Reduction Pair Processor
Using the linear polynomial interpretation over the naturals
[top#0(x1)] |
= |
1 · x1
|
[ok0(x1)] |
= |
1 |
[f00(x1, x2)] |
= |
1 · x1
|
[active0(x1)] |
= |
0 |
[f01(x1, x2)] |
= |
0 |
[ok1(x1)] |
= |
0 |
[f10(x1, x2)] |
= |
0 |
[active1(x1)] |
= |
0 |
[f11(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[mark1(x1)] |
= |
0 |
[proper1(x1)] |
= |
0 |
[proper0(x1)] |
= |
1 |
[a] |
= |
0 |
[b] |
= |
0 |
[mark0(x1)] |
= |
0 |
the
pairs
top#0(ok0(f00(x0,x1))) |
→ |
top#0(f00(active0(x0),x1)) |
(35) |
top#0(ok0(f01(x0,x1))) |
→ |
top#0(f01(active0(x0),x1)) |
(36) |
could be deleted.
1.1.1.1.1.1.1.2.2.1.1.1 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[proper1(x1)] |
= |
1 + 1 · x1
|
[f10(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[f00(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[proper0(x1)] |
= |
1 · x1
|
[f11(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[a] |
= |
0 |
[ok1(x1)] |
= |
1 + 1 · x1
|
[mark0(x1)] |
= |
1 · x1
|
[mark1(x1)] |
= |
1 + 1 · x1
|
[ok0(x1)] |
= |
1 · x1
|
[f01(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[b] |
= |
1 |
[active1(x1)] |
= |
1 + 1 · x1
|
[top#0(x1)] |
= |
1 · x1
|
together with the usable
rules
proper1(f10(X1,X2)) |
→ |
f00(proper1(X1),proper0(X2)) |
(64) |
proper1(f11(X1,X2)) |
→ |
f00(proper1(X1),proper1(X2)) |
(65) |
proper1(a) |
→ |
ok1(a) |
(43) |
f00(mark0(X1),X2) |
→ |
mark0(f00(X1,X2)) |
(45) |
f00(mark1(X1),X2) |
→ |
mark1(f10(X1,X2)) |
(68) |
f00(ok0(X1),ok0(X2)) |
→ |
ok0(f00(X1,X2)) |
(49) |
f00(ok0(X1),ok1(X2)) |
→ |
ok0(f01(X1,X2)) |
(50) |
f00(ok1(X1),ok0(X2)) |
→ |
ok1(f10(X1,X2)) |
(70) |
f00(ok1(X1),ok1(X2)) |
→ |
ok1(f11(X1,X2)) |
(71) |
f01(mark0(X1),X2) |
→ |
mark0(f01(X1,X2)) |
(46) |
f01(mark1(X1),X2) |
→ |
mark1(f11(X1,X2)) |
(69) |
proper0(f00(X1,X2)) |
→ |
f00(proper0(X1),proper0(X2)) |
(39) |
proper0(f01(X1,X2)) |
→ |
f00(proper0(X1),proper1(X2)) |
(40) |
proper0(b) |
→ |
ok0(b) |
(44) |
active1(f11(X,X)) |
→ |
mark1(f10(a,b)) |
(78) |
active1(f10(X1,X2)) |
→ |
f00(active1(X1),X2) |
(75) |
active1(f11(X1,X2)) |
→ |
f01(active1(X1),X2) |
(76) |
(w.r.t. the implicit argument filter of the reduction pair),
the
rule
could be deleted.
1.1.1.1.1.1.1.2.2.1.1.1.1 Monotonic Reduction Pair Processor
Using the linear polynomial interpretation over the naturals
[proper1(x1)] |
= |
1 + 1 · x1
|
[f10(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[f00(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[proper0(x1)] |
= |
1 · x1
|
[f11(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[a] |
= |
0 |
[ok1(x1)] |
= |
1 + 1 · x1
|
[mark0(x1)] |
= |
1 · x1
|
[mark1(x1)] |
= |
1 + 1 · x1
|
[ok0(x1)] |
= |
1 · x1
|
[f01(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[b] |
= |
0 |
[active1(x1)] |
= |
1 + 1 · x1
|
[top#0(x1)] |
= |
1 · x1
|
the
rule
active1(f11(X,X)) |
→ |
mark1(f10(a,b)) |
(78) |
could be deleted.
1.1.1.1.1.1.1.2.2.1.1.1.1.1 Monotonic Reduction Pair Processor
Using the linear polynomial interpretation over the naturals
[proper1(x1)] |
= |
1 + 1 · x1
|
[f10(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[f00(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[proper0(x1)] |
= |
1 · x1
|
[f11(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[a] |
= |
0 |
[ok1(x1)] |
= |
1 + 1 · x1
|
[mark0(x1)] |
= |
1 · x1
|
[mark1(x1)] |
= |
1 + 1 · x1
|
[ok0(x1)] |
= |
1 · x1
|
[f01(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[b] |
= |
0 |
[active1(x1)] |
= |
1 · x1
|
[top#0(x1)] |
= |
1 · x1
|
the
pairs
top#0(ok1(f10(x0,x1))) |
→ |
top#0(f00(active1(x0),x1)) |
(60) |
top#0(ok1(f11(x0,x1))) |
→ |
top#0(f01(active1(x0),x1)) |
(61) |
and
no rules
could be deleted.
1.1.1.1.1.1.1.2.2.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[proper1(x1)] |
= |
1 · x1
|
[f10(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[f00(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[proper0(x1)] |
= |
1 · x1
|
[f11(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[a] |
= |
0 |
[ok1(x1)] |
= |
1 · x1
|
[mark0(x1)] |
= |
1 · x1
|
[mark1(x1)] |
= |
1 + 1 · x1
|
[ok0(x1)] |
= |
1 · x1
|
[f01(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
[b] |
= |
0 |
[top#0(x1)] |
= |
1 · x1
|
together with the usable
rules
proper1(f10(X1,X2)) |
→ |
f00(proper1(X1),proper0(X2)) |
(64) |
proper1(f11(X1,X2)) |
→ |
f00(proper1(X1),proper1(X2)) |
(65) |
proper1(a) |
→ |
ok1(a) |
(43) |
f00(mark0(X1),X2) |
→ |
mark0(f00(X1,X2)) |
(45) |
f00(mark1(X1),X2) |
→ |
mark1(f10(X1,X2)) |
(68) |
f00(ok0(X1),ok0(X2)) |
→ |
ok0(f00(X1,X2)) |
(49) |
f00(ok0(X1),ok1(X2)) |
→ |
ok0(f01(X1,X2)) |
(50) |
f00(ok1(X1),ok0(X2)) |
→ |
ok1(f10(X1,X2)) |
(70) |
f00(ok1(X1),ok1(X2)) |
→ |
ok1(f11(X1,X2)) |
(71) |
f01(mark0(X1),X2) |
→ |
mark0(f01(X1,X2)) |
(46) |
f01(mark1(X1),X2) |
→ |
mark1(f11(X1,X2)) |
(69) |
proper0(f00(X1,X2)) |
→ |
f00(proper0(X1),proper0(X2)) |
(39) |
proper0(f01(X1,X2)) |
→ |
f00(proper0(X1),proper1(X2)) |
(40) |
proper0(b) |
→ |
ok0(b) |
(44) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
top#0(mark1(f10(x0,x1))) |
→ |
top#0(f00(proper1(x0),proper0(x1))) |
(62) |
top#0(mark1(f11(x0,x1))) |
→ |
top#0(f00(proper1(x0),proper1(x1))) |
(63) |
and
no rules
could be deleted.
1.1.1.1.1.1.1.2.2.1.1.1.1.1.1.1 P is empty
There are no pairs anymore.