The rewrite relation of the following TRS is considered.
active(f(a,b,X)) | → | mark(f(X,X,X)) | (1) |
active(c) | → | mark(a) | (2) |
active(c) | → | mark(b) | (3) |
active(f(X1,X2,X3)) | → | f(X1,X2,active(X3)) | (4) |
f(X1,X2,mark(X3)) | → | mark(f(X1,X2,X3)) | (5) |
proper(f(X1,X2,X3)) | → | f(proper(X1),proper(X2),proper(X3)) | (6) |
proper(a) | → | ok(a) | (7) |
proper(b) | → | ok(b) | (8) |
proper(c) | → | ok(c) | (9) |
f(ok(X1),ok(X2),ok(X3)) | → | ok(f(X1,X2,X3)) | (10) |
top(mark(X)) | → | top(proper(X)) | (11) |
top(ok(X)) | → | top(active(X)) | (12) |
active#(f(a,b,X)) | → | f#(X,X,X) | (13) |
active#(f(X1,X2,X3)) | → | f#(X1,X2,active(X3)) | (14) |
active#(f(X1,X2,X3)) | → | active#(X3) | (15) |
f#(X1,X2,mark(X3)) | → | f#(X1,X2,X3) | (16) |
proper#(f(X1,X2,X3)) | → | f#(proper(X1),proper(X2),proper(X3)) | (17) |
proper#(f(X1,X2,X3)) | → | proper#(X1) | (18) |
proper#(f(X1,X2,X3)) | → | proper#(X2) | (19) |
proper#(f(X1,X2,X3)) | → | proper#(X3) | (20) |
f#(ok(X1),ok(X2),ok(X3)) | → | f#(X1,X2,X3) | (21) |
top#(mark(X)) | → | top#(proper(X)) | (22) |
top#(mark(X)) | → | proper#(X) | (23) |
top#(ok(X)) | → | top#(active(X)) | (24) |
top#(ok(X)) | → | active#(X) | (25) |
The dependency pairs are split into 4 components.
top#(ok(X)) | → | top#(active(X)) | (24) |
top#(mark(X)) | → | top#(proper(X)) | (22) |
[proper(x1)] | = | 1 · x1 |
[f(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[a] | = | 0 |
[ok(x1)] | = | 2 · x1 |
[b] | = | 0 |
[c] | = | 0 |
[mark(x1)] | = | 1 · x1 |
[active(x1)] | = | 2 · x1 |
[top#(x1)] | = | 1 · x1 |
proper(f(X1,X2,X3)) | → | f(proper(X1),proper(X2),proper(X3)) | (6) |
proper(a) | → | ok(a) | (7) |
proper(b) | → | ok(b) | (8) |
proper(c) | → | ok(c) | (9) |
f(X1,X2,mark(X3)) | → | mark(f(X1,X2,X3)) | (5) |
f(ok(X1),ok(X2),ok(X3)) | → | ok(f(X1,X2,X3)) | (10) |
active(f(a,b,X)) | → | mark(f(X,X,X)) | (1) |
active(c) | → | mark(a) | (2) |
active(c) | → | mark(b) | (3) |
active(f(X1,X2,X3)) | → | f(X1,X2,active(X3)) | (4) |
top#(ok(f(a,b,x0))) | → | top#(mark(f(x0,x0,x0))) | (26) |
top#(ok(c)) | → | top#(mark(a)) | (27) |
top#(ok(c)) | → | top#(mark(b)) | (28) |
top#(ok(f(x0,x1,x2))) | → | top#(f(x0,x1,active(x2))) | (29) |
top#(mark(f(x0,x1,x2))) | → | top#(f(proper(x0),proper(x1),proper(x2))) | (30) |
top#(mark(a)) | → | top#(ok(a)) | (31) |
top#(mark(b)) | → | top#(ok(b)) | (32) |
top#(mark(c)) | → | top#(ok(c)) | (33) |
The dependency pairs are split into 1 component.
top#(mark(f(x0,x1,x2))) | → | top#(f(proper(x0),proper(x1),proper(x2))) | (30) |
top#(ok(f(a,b,x0))) | → | top#(mark(f(x0,x0,x0))) | (26) |
top#(ok(f(x0,x1,x2))) | → | top#(f(x0,x1,active(x2))) | (29) |
As carrier we take the set {0,1}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 2):
[a] | = | 1 |
[active(x1)] | = | 0 |
[b] | = | 0 |
[c] | = | 0 |
[proper(x1)] | = | 1x1 |
[f(x1, x2, x3)] | = | 0 |
[top#(x1)] | = | 0 |
[ok(x1)] | = | 1x1 |
[mark(x1)] | = | 0 |
top#0(mark0(f000(x0,x1,x2))) | → | top#0(f000(proper0(x0),proper0(x1),proper0(x2))) | (34) |
top#0(ok0(f100(a,b,x0))) | → | top#0(mark0(f000(x0,x0,x0))) | (35) |
top#0(ok0(f101(a,b,x0))) | → | top#0(mark0(f111(x0,x0,x0))) | (36) |
top#0(mark0(f001(x0,x1,x2))) | → | top#0(f001(proper0(x0),proper0(x1),proper1(x2))) | (37) |
top#0(mark0(f010(x0,x1,x2))) | → | top#0(f010(proper0(x0),proper1(x1),proper0(x2))) | (38) |
top#0(mark0(f011(x0,x1,x2))) | → | top#0(f011(proper0(x0),proper1(x1),proper1(x2))) | (39) |
top#0(mark0(f100(x0,x1,x2))) | → | top#0(f100(proper1(x0),proper0(x1),proper0(x2))) | (40) |
top#0(mark0(f101(x0,x1,x2))) | → | top#0(f101(proper1(x0),proper0(x1),proper1(x2))) | (41) |
top#0(mark0(f110(x0,x1,x2))) | → | top#0(f110(proper1(x0),proper1(x1),proper0(x2))) | (42) |
top#0(mark0(f111(x0,x1,x2))) | → | top#0(f111(proper1(x0),proper1(x1),proper1(x2))) | (43) |
top#0(ok0(f000(x0,x1,x2))) | → | top#0(f000(x0,x1,active0(x2))) | (44) |
top#0(ok0(f001(x0,x1,x2))) | → | top#0(f000(x0,x1,active1(x2))) | (45) |
top#0(ok0(f010(x0,x1,x2))) | → | top#0(f010(x0,x1,active0(x2))) | (46) |
top#0(ok0(f011(x0,x1,x2))) | → | top#0(f010(x0,x1,active1(x2))) | (47) |
top#0(ok0(f100(x0,x1,x2))) | → | top#0(f100(x0,x1,active0(x2))) | (48) |
top#0(ok0(f101(x0,x1,x2))) | → | top#0(f100(x0,x1,active1(x2))) | (49) |
top#0(ok0(f110(x0,x1,x2))) | → | top#0(f110(x0,x1,active0(x2))) | (50) |
top#0(ok0(f111(x0,x1,x2))) | → | top#0(f110(x0,x1,active1(x2))) | (51) |
proper0(f000(X1,X2,X3)) | → | f000(proper0(X1),proper0(X2),proper0(X3)) | (52) |
proper0(f001(X1,X2,X3)) | → | f001(proper0(X1),proper0(X2),proper1(X3)) | (53) |
proper0(f010(X1,X2,X3)) | → | f010(proper0(X1),proper1(X2),proper0(X3)) | (54) |
proper0(f011(X1,X2,X3)) | → | f011(proper0(X1),proper1(X2),proper1(X3)) | (55) |
proper0(f100(X1,X2,X3)) | → | f100(proper1(X1),proper0(X2),proper0(X3)) | (56) |
proper0(f101(X1,X2,X3)) | → | f101(proper1(X1),proper0(X2),proper1(X3)) | (57) |
proper0(f110(X1,X2,X3)) | → | f110(proper1(X1),proper1(X2),proper0(X3)) | (58) |
proper0(f111(X1,X2,X3)) | → | f111(proper1(X1),proper1(X2),proper1(X3)) | (59) |
proper1(a) | → | ok1(a) | (60) |
proper0(b) | → | ok0(b) | (61) |
proper0(c) | → | ok0(c) | (62) |
f000(X1,X2,mark0(X3)) | → | mark0(f000(X1,X2,X3)) | (63) |
f000(X1,X2,mark1(X3)) | → | mark0(f001(X1,X2,X3)) | (64) |
f010(X1,X2,mark0(X3)) | → | mark0(f010(X1,X2,X3)) | (65) |
f010(X1,X2,mark1(X3)) | → | mark0(f011(X1,X2,X3)) | (66) |
f100(X1,X2,mark0(X3)) | → | mark0(f100(X1,X2,X3)) | (67) |
f100(X1,X2,mark1(X3)) | → | mark0(f101(X1,X2,X3)) | (68) |
f110(X1,X2,mark0(X3)) | → | mark0(f110(X1,X2,X3)) | (69) |
f110(X1,X2,mark1(X3)) | → | mark0(f111(X1,X2,X3)) | (70) |
f000(ok0(X1),ok0(X2),ok0(X3)) | → | ok0(f000(X1,X2,X3)) | (71) |
f001(ok0(X1),ok0(X2),ok1(X3)) | → | ok0(f001(X1,X2,X3)) | (72) |
f010(ok0(X1),ok1(X2),ok0(X3)) | → | ok0(f010(X1,X2,X3)) | (73) |
f011(ok0(X1),ok1(X2),ok1(X3)) | → | ok0(f011(X1,X2,X3)) | (74) |
f100(ok1(X1),ok0(X2),ok0(X3)) | → | ok0(f100(X1,X2,X3)) | (75) |
f101(ok1(X1),ok0(X2),ok1(X3)) | → | ok0(f101(X1,X2,X3)) | (76) |
f110(ok1(X1),ok1(X2),ok0(X3)) | → | ok0(f110(X1,X2,X3)) | (77) |
f111(ok1(X1),ok1(X2),ok1(X3)) | → | ok0(f111(X1,X2,X3)) | (78) |
active0(f100(a,b,X)) | → | mark0(f000(X,X,X)) | (79) |
active0(f101(a,b,X)) | → | mark0(f111(X,X,X)) | (80) |
active0(c) | → | mark1(a) | (81) |
active0(c) | → | mark0(b) | (82) |
active0(f000(X1,X2,X3)) | → | f000(X1,X2,active0(X3)) | (83) |
active0(f001(X1,X2,X3)) | → | f000(X1,X2,active1(X3)) | (84) |
active0(f010(X1,X2,X3)) | → | f010(X1,X2,active0(X3)) | (85) |
active0(f011(X1,X2,X3)) | → | f010(X1,X2,active1(X3)) | (86) |
active0(f100(X1,X2,X3)) | → | f100(X1,X2,active0(X3)) | (87) |
active0(f101(X1,X2,X3)) | → | f100(X1,X2,active1(X3)) | (88) |
active0(f110(X1,X2,X3)) | → | f110(X1,X2,active0(X3)) | (89) |
active0(f111(X1,X2,X3)) | → | f110(X1,X2,active1(X3)) | (90) |
The dependency pairs are split into 1 component.
top#0(ok0(f100(a,b,x0))) | → | top#0(mark0(f000(x0,x0,x0))) | (35) |
top#0(mark0(f000(x0,x1,x2))) | → | top#0(f000(proper0(x0),proper0(x1),proper0(x2))) | (34) |
top#0(ok0(f101(a,b,x0))) | → | top#0(mark0(f111(x0,x0,x0))) | (36) |
top#0(mark0(f001(x0,x1,x2))) | → | top#0(f001(proper0(x0),proper0(x1),proper1(x2))) | (37) |
top#0(ok0(f000(x0,x1,x2))) | → | top#0(f000(x0,x1,active0(x2))) | (44) |
top#0(ok0(f010(x0,x1,x2))) | → | top#0(f010(x0,x1,active0(x2))) | (46) |
top#0(ok0(f100(x0,x1,x2))) | → | top#0(f100(x0,x1,active0(x2))) | (48) |
top#0(ok0(f110(x0,x1,x2))) | → | top#0(f110(x0,x1,active0(x2))) | (50) |
top#0(mark0(f010(x0,x1,x2))) | → | top#0(f010(proper0(x0),proper1(x1),proper0(x2))) | (38) |
top#0(mark0(f011(x0,x1,x2))) | → | top#0(f011(proper0(x0),proper1(x1),proper1(x2))) | (39) |
top#0(mark0(f100(x0,x1,x2))) | → | top#0(f100(proper1(x0),proper0(x1),proper0(x2))) | (40) |
top#0(mark0(f101(x0,x1,x2))) | → | top#0(f101(proper1(x0),proper0(x1),proper1(x2))) | (41) |
top#0(mark0(f110(x0,x1,x2))) | → | top#0(f110(proper1(x0),proper1(x1),proper0(x2))) | (42) |
top#0(mark0(f111(x0,x1,x2))) | → | top#0(f111(proper1(x0),proper1(x1),proper1(x2))) | (43) |
[top#0(x1)] | = | 1 · x1 |
[ok0(x1)] | = | 1 · x1 |
[f100(x1, x2, x3)] | = | 1 + 1 · x1 |
[a] | = | 1 |
[b] | = | 0 |
[mark0(x1)] | = | 1 · x1 |
[f000(x1, x2, x3)] | = | 0 |
[proper0(x1)] | = | 0 |
[f101(x1, x2, x3)] | = | 1 · x1 |
[f111(x1, x2, x3)] | = | 0 |
[f001(x1, x2, x3)] | = | 0 |
[proper1(x1)] | = | 1 · x1 |
[active0(x1)] | = | 0 |
[f010(x1, x2, x3)] | = | 0 |
[f110(x1, x2, x3)] | = | 0 |
[f011(x1, x2, x3)] | = | 0 |
[mark1(x1)] | = | 0 |
[c] | = | 0 |
[ok1(x1)] | = | 1 · x1 |
[active1(x1)] | = | 1 · x1 |
f000(X1,X2,mark0(X3)) | → | mark0(f000(X1,X2,X3)) | (63) |
f000(X1,X2,mark1(X3)) | → | mark0(f001(X1,X2,X3)) | (64) |
f000(ok0(X1),ok0(X2),ok0(X3)) | → | ok0(f000(X1,X2,X3)) | (71) |
f111(ok1(X1),ok1(X2),ok1(X3)) | → | ok0(f111(X1,X2,X3)) | (78) |
proper1(a) | → | ok1(a) | (60) |
f001(ok0(X1),ok0(X2),ok1(X3)) | → | ok0(f001(X1,X2,X3)) | (72) |
f010(X1,X2,mark0(X3)) | → | mark0(f010(X1,X2,X3)) | (65) |
f010(X1,X2,mark1(X3)) | → | mark0(f011(X1,X2,X3)) | (66) |
f010(ok0(X1),ok1(X2),ok0(X3)) | → | ok0(f010(X1,X2,X3)) | (73) |
f100(X1,X2,mark0(X3)) | → | mark0(f100(X1,X2,X3)) | (67) |
f100(X1,X2,mark1(X3)) | → | mark0(f101(X1,X2,X3)) | (68) |
f100(ok1(X1),ok0(X2),ok0(X3)) | → | ok0(f100(X1,X2,X3)) | (75) |
f110(X1,X2,mark0(X3)) | → | mark0(f110(X1,X2,X3)) | (69) |
f110(X1,X2,mark1(X3)) | → | mark0(f111(X1,X2,X3)) | (70) |
f110(ok1(X1),ok1(X2),ok0(X3)) | → | ok0(f110(X1,X2,X3)) | (77) |
f011(ok0(X1),ok1(X2),ok1(X3)) | → | ok0(f011(X1,X2,X3)) | (74) |
f101(ok1(X1),ok0(X2),ok1(X3)) | → | ok0(f101(X1,X2,X3)) | (76) |
top#0(ok0(f100(a,b,x0))) | → | top#0(mark0(f000(x0,x0,x0))) | (35) |
top#0(ok0(f101(a,b,x0))) | → | top#0(mark0(f111(x0,x0,x0))) | (36) |
[top#0(x1)] | = | 1 · x1 |
[mark0(x1)] | = | 1 |
[f000(x1, x2, x3)] | = | 1 |
[proper0(x1)] | = | 0 |
[f001(x1, x2, x3)] | = | 0 |
[proper1(x1)] | = | 0 |
[ok0(x1)] | = | 1 · x1 |
[active0(x1)] | = | 0 |
[f010(x1, x2, x3)] | = | 1 |
[f100(x1, x2, x3)] | = | 1 |
[f110(x1, x2, x3)] | = | 1 |
[f011(x1, x2, x3)] | = | 0 |
[f101(x1, x2, x3)] | = | 0 |
[f111(x1, x2, x3)] | = | 0 |
[b] | = | 0 |
[c] | = | 0 |
[mark1(x1)] | = | 0 |
[a] | = | 0 |
[ok1(x1)] | = | 0 |
[active1(x1)] | = | 1 · x1 |
f000(X1,X2,mark0(X3)) | → | mark0(f000(X1,X2,X3)) | (63) |
f000(X1,X2,mark1(X3)) | → | mark0(f001(X1,X2,X3)) | (64) |
f000(ok0(X1),ok0(X2),ok0(X3)) | → | ok0(f000(X1,X2,X3)) | (71) |
f001(ok0(X1),ok0(X2),ok1(X3)) | → | ok0(f001(X1,X2,X3)) | (72) |
f010(X1,X2,mark0(X3)) | → | mark0(f010(X1,X2,X3)) | (65) |
f010(X1,X2,mark1(X3)) | → | mark0(f011(X1,X2,X3)) | (66) |
f010(ok0(X1),ok1(X2),ok0(X3)) | → | ok0(f010(X1,X2,X3)) | (73) |
f100(X1,X2,mark0(X3)) | → | mark0(f100(X1,X2,X3)) | (67) |
f100(X1,X2,mark1(X3)) | → | mark0(f101(X1,X2,X3)) | (68) |
f100(ok1(X1),ok0(X2),ok0(X3)) | → | ok0(f100(X1,X2,X3)) | (75) |
f110(X1,X2,mark0(X3)) | → | mark0(f110(X1,X2,X3)) | (69) |
f110(X1,X2,mark1(X3)) | → | mark0(f111(X1,X2,X3)) | (70) |
f110(ok1(X1),ok1(X2),ok0(X3)) | → | ok0(f110(X1,X2,X3)) | (77) |
f011(ok0(X1),ok1(X2),ok1(X3)) | → | ok0(f011(X1,X2,X3)) | (74) |
f101(ok1(X1),ok0(X2),ok1(X3)) | → | ok0(f101(X1,X2,X3)) | (76) |
f111(ok1(X1),ok1(X2),ok1(X3)) | → | ok0(f111(X1,X2,X3)) | (78) |
top#0(mark0(f001(x0,x1,x2))) | → | top#0(f001(proper0(x0),proper0(x1),proper1(x2))) | (37) |
top#0(mark0(f011(x0,x1,x2))) | → | top#0(f011(proper0(x0),proper1(x1),proper1(x2))) | (39) |
top#0(mark0(f101(x0,x1,x2))) | → | top#0(f101(proper1(x0),proper0(x1),proper1(x2))) | (41) |
top#0(mark0(f111(x0,x1,x2))) | → | top#0(f111(proper1(x0),proper1(x1),proper1(x2))) | (43) |
[top#0(x1)] | = | 1 · x1 |
[mark0(x1)] | = | 1 + 1 · x1 |
[f000(x1, x2, x3)] | = | 1 · x3 |
[proper0(x1)] | = | 1 · x1 |
[ok0(x1)] | = | 1 · x1 |
[active0(x1)] | = | 1 · x1 |
[f010(x1, x2, x3)] | = | 1 + 1 · x3 |
[f100(x1, x2, x3)] | = | 1 + 1 · x3 |
[f110(x1, x2, x3)] | = | 1 · x3 |
[proper1(x1)] | = | 0 |
[f001(x1, x2, x3)] | = | 0 |
[f011(x1, x2, x3)] | = | 1 |
[f101(x1, x2, x3)] | = | 1 |
[f111(x1, x2, x3)] | = | 0 |
[b] | = | 0 |
[c] | = | 1 |
[mark1(x1)] | = | 1 |
[a] | = | 0 |
[active1(x1)] | = | 0 |
[ok1(x1)] | = | 0 |
proper0(f000(X1,X2,X3)) | → | f000(proper0(X1),proper0(X2),proper0(X3)) | (52) |
proper0(f001(X1,X2,X3)) | → | f001(proper0(X1),proper0(X2),proper1(X3)) | (53) |
proper0(f010(X1,X2,X3)) | → | f010(proper0(X1),proper1(X2),proper0(X3)) | (54) |
proper0(f011(X1,X2,X3)) | → | f011(proper0(X1),proper1(X2),proper1(X3)) | (55) |
proper0(f100(X1,X2,X3)) | → | f100(proper1(X1),proper0(X2),proper0(X3)) | (56) |
proper0(f101(X1,X2,X3)) | → | f101(proper1(X1),proper0(X2),proper1(X3)) | (57) |
proper0(f110(X1,X2,X3)) | → | f110(proper1(X1),proper1(X2),proper0(X3)) | (58) |
proper0(f111(X1,X2,X3)) | → | f111(proper1(X1),proper1(X2),proper1(X3)) | (59) |
proper0(b) | → | ok0(b) | (61) |
proper0(c) | → | ok0(c) | (62) |
f000(X1,X2,mark0(X3)) | → | mark0(f000(X1,X2,X3)) | (63) |
f000(X1,X2,mark1(X3)) | → | mark0(f001(X1,X2,X3)) | (64) |
f000(ok0(X1),ok0(X2),ok0(X3)) | → | ok0(f000(X1,X2,X3)) | (71) |
active0(f100(a,b,X)) | → | mark0(f000(X,X,X)) | (79) |
active0(f101(a,b,X)) | → | mark0(f111(X,X,X)) | (80) |
active0(c) | → | mark1(a) | (81) |
active0(c) | → | mark0(b) | (82) |
active0(f000(X1,X2,X3)) | → | f000(X1,X2,active0(X3)) | (83) |
active0(f001(X1,X2,X3)) | → | f000(X1,X2,active1(X3)) | (84) |
active0(f010(X1,X2,X3)) | → | f010(X1,X2,active0(X3)) | (85) |
active0(f011(X1,X2,X3)) | → | f010(X1,X2,active1(X3)) | (86) |
active0(f100(X1,X2,X3)) | → | f100(X1,X2,active0(X3)) | (87) |
active0(f101(X1,X2,X3)) | → | f100(X1,X2,active1(X3)) | (88) |
active0(f110(X1,X2,X3)) | → | f110(X1,X2,active0(X3)) | (89) |
active0(f111(X1,X2,X3)) | → | f110(X1,X2,active1(X3)) | (90) |
f010(X1,X2,mark0(X3)) | → | mark0(f010(X1,X2,X3)) | (65) |
f010(X1,X2,mark1(X3)) | → | mark0(f011(X1,X2,X3)) | (66) |
f010(ok0(X1),ok1(X2),ok0(X3)) | → | ok0(f010(X1,X2,X3)) | (73) |
f100(X1,X2,mark0(X3)) | → | mark0(f100(X1,X2,X3)) | (67) |
f100(X1,X2,mark1(X3)) | → | mark0(f101(X1,X2,X3)) | (68) |
f100(ok1(X1),ok0(X2),ok0(X3)) | → | ok0(f100(X1,X2,X3)) | (75) |
f110(X1,X2,mark0(X3)) | → | mark0(f110(X1,X2,X3)) | (69) |
f110(X1,X2,mark1(X3)) | → | mark0(f111(X1,X2,X3)) | (70) |
f110(ok1(X1),ok1(X2),ok0(X3)) | → | ok0(f110(X1,X2,X3)) | (77) |
f001(ok0(X1),ok0(X2),ok1(X3)) | → | ok0(f001(X1,X2,X3)) | (72) |
f011(ok0(X1),ok1(X2),ok1(X3)) | → | ok0(f011(X1,X2,X3)) | (74) |
f101(ok1(X1),ok0(X2),ok1(X3)) | → | ok0(f101(X1,X2,X3)) | (76) |
f111(ok1(X1),ok1(X2),ok1(X3)) | → | ok0(f111(X1,X2,X3)) | (78) |
top#0(mark0(f000(x0,x1,x2))) | → | top#0(f000(proper0(x0),proper0(x1),proper0(x2))) | (34) |
top#0(mark0(f010(x0,x1,x2))) | → | top#0(f010(proper0(x0),proper1(x1),proper0(x2))) | (38) |
top#0(mark0(f100(x0,x1,x2))) | → | top#0(f100(proper1(x0),proper0(x1),proper0(x2))) | (40) |
top#0(mark0(f110(x0,x1,x2))) | → | top#0(f110(proper1(x0),proper1(x1),proper0(x2))) | (42) |
[top#0(x1)] | = | 1 · x1 |
[ok0(x1)] | = | 1 + 1 · x1 |
[f000(x1, x2, x3)] | = | 1 · x1 |
[active0(x1)] | = | 0 |
[f010(x1, x2, x3)] | = | 1 · x1 |
[f100(x1, x2, x3)] | = | 1 · x1 |
[f110(x1, x2, x3)] | = | 1 · x1 |
[a] | = | 0 |
[b] | = | 0 |
[mark0(x1)] | = | 0 |
[f101(x1, x2, x3)] | = | 0 |
[f111(x1, x2, x3)] | = | 0 |
[c] | = | 0 |
[mark1(x1)] | = | 0 |
[f001(x1, x2, x3)] | = | 1 · x1 |
[active1(x1)] | = | 1 · x1 |
[f011(x1, x2, x3)] | = | 1 · x1 |
[ok1(x1)] | = | 1 + 1 · x1 |
f000(X1,X2,mark0(X3)) | → | mark0(f000(X1,X2,X3)) | (63) |
f000(X1,X2,mark1(X3)) | → | mark0(f001(X1,X2,X3)) | (64) |
f000(ok0(X1),ok0(X2),ok0(X3)) | → | ok0(f000(X1,X2,X3)) | (71) |
f010(X1,X2,mark0(X3)) | → | mark0(f010(X1,X2,X3)) | (65) |
f010(X1,X2,mark1(X3)) | → | mark0(f011(X1,X2,X3)) | (66) |
f010(ok0(X1),ok1(X2),ok0(X3)) | → | ok0(f010(X1,X2,X3)) | (73) |
f100(X1,X2,mark0(X3)) | → | mark0(f100(X1,X2,X3)) | (67) |
f100(X1,X2,mark1(X3)) | → | mark0(f101(X1,X2,X3)) | (68) |
f100(ok1(X1),ok0(X2),ok0(X3)) | → | ok0(f100(X1,X2,X3)) | (75) |
f110(X1,X2,mark0(X3)) | → | mark0(f110(X1,X2,X3)) | (69) |
f110(X1,X2,mark1(X3)) | → | mark0(f111(X1,X2,X3)) | (70) |
f110(ok1(X1),ok1(X2),ok0(X3)) | → | ok0(f110(X1,X2,X3)) | (77) |
top#0(ok0(f000(x0,x1,x2))) | → | top#0(f000(x0,x1,active0(x2))) | (44) |
top#0(ok0(f010(x0,x1,x2))) | → | top#0(f010(x0,x1,active0(x2))) | (46) |
top#0(ok0(f100(x0,x1,x2))) | → | top#0(f100(x0,x1,active0(x2))) | (48) |
top#0(ok0(f110(x0,x1,x2))) | → | top#0(f110(x0,x1,active0(x2))) | (50) |
There are no pairs anymore.
active#(f(X1,X2,X3)) | → | active#(X3) | (15) |
[f(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[active#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
active#(f(X1,X2,X3)) | → | active#(X3) | (15) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
proper#(f(X1,X2,X3)) | → | proper#(X2) | (19) |
proper#(f(X1,X2,X3)) | → | proper#(X1) | (18) |
proper#(f(X1,X2,X3)) | → | proper#(X3) | (20) |
[f(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[proper#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
proper#(f(X1,X2,X3)) | → | proper#(X2) | (19) |
1 | > | 1 | |
proper#(f(X1,X2,X3)) | → | proper#(X1) | (18) |
1 | > | 1 | |
proper#(f(X1,X2,X3)) | → | proper#(X3) | (20) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
f#(ok(X1),ok(X2),ok(X3)) | → | f#(X1,X2,X3) | (21) |
f#(X1,X2,mark(X3)) | → | f#(X1,X2,X3) | (16) |
[ok(x1)] | = | 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[f#(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
f#(ok(X1),ok(X2),ok(X3)) | → | f#(X1,X2,X3) | (21) |
1 | > | 1 | |
2 | > | 2 | |
3 | > | 3 | |
f#(X1,X2,mark(X3)) | → | f#(X1,X2,X3) | (16) |
1 | ≥ | 1 | |
2 | ≥ | 2 | |
3 | > | 3 |
As there is no critical graph in the transitive closure, there are no infinite chains.