The rewrite relation of the following TRS is considered.
active(f(X)) | → | mark(if(X,c,f(true))) | (1) |
active(if(true,X,Y)) | → | mark(X) | (2) |
active(if(false,X,Y)) | → | mark(Y) | (3) |
active(f(X)) | → | f(active(X)) | (4) |
active(if(X1,X2,X3)) | → | if(active(X1),X2,X3) | (5) |
active(if(X1,X2,X3)) | → | if(X1,active(X2),X3) | (6) |
f(mark(X)) | → | mark(f(X)) | (7) |
if(mark(X1),X2,X3) | → | mark(if(X1,X2,X3)) | (8) |
if(X1,mark(X2),X3) | → | mark(if(X1,X2,X3)) | (9) |
proper(f(X)) | → | f(proper(X)) | (10) |
proper(if(X1,X2,X3)) | → | if(proper(X1),proper(X2),proper(X3)) | (11) |
proper(c) | → | ok(c) | (12) |
proper(true) | → | ok(true) | (13) |
proper(false) | → | ok(false) | (14) |
f(ok(X)) | → | ok(f(X)) | (15) |
if(ok(X1),ok(X2),ok(X3)) | → | ok(if(X1,X2,X3)) | (16) |
top(mark(X)) | → | top(proper(X)) | (17) |
top(ok(X)) | → | top(active(X)) | (18) |
[if(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[true] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[false] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[c] | = |
|
active(if(false,X,Y)) | → | mark(Y) | (3) |
[if(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[true] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[false] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[c] | = |
|
top(mark(X)) | → | top(proper(X)) | (17) |
[if(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 16 · x3 + 0 |
[ok(x1)] | = | 1 · x1 + 0 |
[active(x1)] | = | 1 · x1 + 0 |
[true] | = | 0 |
[mark(x1)] | = | 1 · x1 + 0 |
[f(x1)] | = | 1 · x1 + 0 |
[proper(x1)] | = | 4 · x1 + 0 |
[top(x1)] | = | 8 · x1 + 30 |
[false] | = | 8 |
[c] | = | 0 |
proper(false) | → | ok(false) | (14) |
[if(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[true] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[c] | = |
|
active(if(true,X,Y)) | → | mark(X) | (2) |
[if(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[true] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[c] | = |
|
top(ok(X)) | → | top(active(X)) | (18) |
[if(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[true] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||||||||||||||
[c] | = |
|
active(f(X)) | → | mark(if(X,c,f(true))) | (1) |
active#(f(X)) | → | active#(X) | (19) |
active#(f(X)) | → | f#(active(X)) | (20) |
active#(if(X1,X2,X3)) | → | active#(X1) | (21) |
active#(if(X1,X2,X3)) | → | if#(active(X1),X2,X3) | (22) |
active#(if(X1,X2,X3)) | → | active#(X2) | (23) |
active#(if(X1,X2,X3)) | → | if#(X1,active(X2),X3) | (24) |
f#(mark(X)) | → | f#(X) | (25) |
if#(mark(X1),X2,X3) | → | if#(X1,X2,X3) | (26) |
if#(X1,mark(X2),X3) | → | if#(X1,X2,X3) | (27) |
proper#(f(X)) | → | proper#(X) | (28) |
proper#(f(X)) | → | f#(proper(X)) | (29) |
proper#(if(X1,X2,X3)) | → | proper#(X3) | (30) |
proper#(if(X1,X2,X3)) | → | proper#(X2) | (31) |
proper#(if(X1,X2,X3)) | → | proper#(X1) | (32) |
proper#(if(X1,X2,X3)) | → | if#(proper(X1),proper(X2),proper(X3)) | (33) |
f#(ok(X)) | → | f#(X) | (34) |
if#(ok(X1),ok(X2),ok(X3)) | → | if#(X1,X2,X3) | (35) |
The dependency pairs are split into 4 components.
active#(if(X1,X2,X3)) | → | active#(X2) | (23) |
active#(f(X)) | → | active#(X) | (19) |
active#(if(X1,X2,X3)) | → | active#(X1) | (21) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
active#(if(X1,X2,X3)) | → | active#(X2) | (23) |
1 | > | 1 | |
active#(f(X)) | → | active#(X) | (19) |
1 | > | 1 | |
active#(if(X1,X2,X3)) | → | active#(X1) | (21) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
proper#(if(X1,X2,X3)) | → | proper#(X3) | (30) |
proper#(f(X)) | → | proper#(X) | (28) |
proper#(if(X1,X2,X3)) | → | proper#(X2) | (31) |
proper#(if(X1,X2,X3)) | → | proper#(X1) | (32) |
π(proper#) | = | 1 |
proper#(if(X1,X2,X3)) | → | proper#(X3) | (30) |
proper#(f(X)) | → | proper#(X) | (28) |
proper#(if(X1,X2,X3)) | → | proper#(X2) | (31) |
proper#(if(X1,X2,X3)) | → | proper#(X1) | (32) |
There are no pairs anymore.
if#(mark(X1),X2,X3) | → | if#(X1,X2,X3) | (26) |
if#(X1,mark(X2),X3) | → | if#(X1,X2,X3) | (27) |
if#(ok(X1),ok(X2),ok(X3)) | → | if#(X1,X2,X3) | (35) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
if#(mark(X1),X2,X3) | → | if#(X1,X2,X3) | (26) |
3 | ≥ | 3 | |
2 | ≥ | 2 | |
1 | > | 1 | |
if#(X1,mark(X2),X3) | → | if#(X1,X2,X3) | (27) |
3 | ≥ | 3 | |
2 | > | 2 | |
1 | ≥ | 1 | |
if#(ok(X1),ok(X2),ok(X3)) | → | if#(X1,X2,X3) | (35) |
3 | > | 3 | |
2 | > | 2 | |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
f#(mark(X)) | → | f#(X) | (25) |
f#(ok(X)) | → | f#(X) | (34) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
f#(mark(X)) | → | f#(X) | (25) |
1 | > | 1 | |
f#(ok(X)) | → | f#(X) | (34) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.