The rewrite relation of the following TRS is considered.
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(X,nil)) | → | mark(X) | (2) |
active(__(nil,X)) | → | mark(X) | (3) |
active(and(tt,X)) | → | mark(X) | (4) |
active(isNePal(__(I,__(P,I)))) | → | mark(tt) | (5) |
active(__(X1,X2)) | → | __(active(X1),X2) | (6) |
active(__(X1,X2)) | → | __(X1,active(X2)) | (7) |
active(and(X1,X2)) | → | and(active(X1),X2) | (8) |
active(isNePal(X)) | → | isNePal(active(X)) | (9) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (10) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (11) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (12) |
isNePal(mark(X)) | → | mark(isNePal(X)) | (13) |
proper(__(X1,X2)) | → | __(proper(X1),proper(X2)) | (14) |
proper(nil) | → | ok(nil) | (15) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (16) |
proper(tt) | → | ok(tt) | (17) |
proper(isNePal(X)) | → | isNePal(proper(X)) | (18) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (19) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (20) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (21) |
top(mark(X)) | → | top(proper(X)) | (22) |
top(ok(X)) | → | top(active(X)) | (23) |
active#(__(X1,X2)) | → | active#(X1) | (24) |
proper#(isNePal(X)) | → | proper#(X) | (25) |
__#(X1,mark(X2)) | → | __#(X1,X2) | (26) |
and#(ok(X1),ok(X2)) | → | and#(X1,X2) | (27) |
and#(mark(X1),X2) | → | and#(X1,X2) | (28) |
proper#(__(X1,X2)) | → | proper#(X1) | (29) |
active#(__(__(X,Y),Z)) | → | __#(X,__(Y,Z)) | (30) |
proper#(and(X1,X2)) | → | proper#(X2) | (31) |
proper#(__(X1,X2)) | → | proper#(X2) | (32) |
active#(__(X1,X2)) | → | __#(X1,active(X2)) | (33) |
active#(__(__(X,Y),Z)) | → | __#(Y,Z) | (34) |
isNePal#(ok(X)) | → | isNePal#(X) | (35) |
top#(ok(X)) | → | top#(active(X)) | (36) |
proper#(__(X1,X2)) | → | __#(proper(X1),proper(X2)) | (37) |
active#(isNePal(X)) | → | active#(X) | (38) |
proper#(isNePal(X)) | → | isNePal#(proper(X)) | (39) |
proper#(and(X1,X2)) | → | proper#(X1) | (40) |
active#(and(X1,X2)) | → | active#(X1) | (41) |
top#(mark(X)) | → | top#(proper(X)) | (42) |
__#(ok(X1),ok(X2)) | → | __#(X1,X2) | (43) |
active#(and(X1,X2)) | → | and#(active(X1),X2) | (44) |
proper#(and(X1,X2)) | → | and#(proper(X1),proper(X2)) | (45) |
__#(mark(X1),X2) | → | __#(X1,X2) | (46) |
isNePal#(mark(X)) | → | isNePal#(X) | (47) |
active#(__(X1,X2)) | → | __#(active(X1),X2) | (48) |
top#(ok(X)) | → | active#(X) | (49) |
active#(__(X1,X2)) | → | active#(X2) | (50) |
active#(isNePal(X)) | → | isNePal#(active(X)) | (51) |
top#(mark(X)) | → | proper#(X) | (52) |
The dependency pairs are split into 6 components.
top#(mark(X)) | → | top#(proper(X)) | (42) |
top#(ok(X)) | → | top#(active(X)) | (36) |
π(top#) | = | 1 |
π(proper) | = | 1 |
π(ok) | = | 1 |
π(proper#) | = | 1 |
π(active) | = | 1 |
π(active#) | = | 1 |
prec(top) | = | 0 | status(top) | = | [] | list-extension(top) | = | Lex | ||
prec(and) | = | 3 | status(and) | = | [2, 1] | list-extension(and) | = | Lex | ||
prec(__#) | = | 0 | status(__#) | = | [1, 2] | list-extension(__#) | = | Lex | ||
prec(isNePal) | = | 2 | status(isNePal) | = | [1] | list-extension(isNePal) | = | Lex | ||
prec(isNePal#) | = | 0 | status(isNePal#) | = | [] | list-extension(isNePal#) | = | Lex | ||
prec(nil) | = | 1 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(mark) | = | 2 | status(mark) | = | [1] | list-extension(mark) | = | Lex | ||
prec(tt) | = | 1 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(and#) | = | 0 | status(and#) | = | [1, 2] | list-extension(and#) | = | Lex | ||
prec(__) | = | 3 | status(__) | = | [1, 2] | list-extension(__) | = | Lex |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[__#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[isNePal(x1)] | = | x1 + 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[tt] | = | 0 |
[and#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[__(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
proper(isNePal(X)) | → | isNePal(proper(X)) | (18) |
active(and(tt,X)) | → | mark(X) | (4) |
proper(nil) | → | ok(nil) | (15) |
active(and(X1,X2)) | → | and(active(X1),X2) | (8) |
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(nil,X)) | → | mark(X) | (3) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (16) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (21) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (19) |
proper(tt) | → | ok(tt) | (17) |
active(isNePal(__(I,__(P,I)))) | → | mark(tt) | (5) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (10) |
active(__(X1,X2)) | → | __(X1,active(X2)) | (7) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (20) |
proper(__(X1,X2)) | → | __(proper(X1),proper(X2)) | (14) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (12) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (11) |
active(isNePal(X)) | → | isNePal(active(X)) | (9) |
isNePal(mark(X)) | → | mark(isNePal(X)) | (13) |
active(__(X1,X2)) | → | __(active(X1),X2) | (6) |
active(__(X,nil)) | → | mark(X) | (2) |
top#(mark(X)) | → | top#(proper(X)) | (42) |
The dependency pairs are split into 1 component.
top#(ok(X)) | → | top#(active(X)) | (36) |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x2 + 0 |
[top#(x1)] | = | x1 + 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 0 |
[proper(x1)] | = | 61699 |
[ok(x1)] | = | x1 + 30101 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 31598 |
[mark(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[active(x1)] | = | x1 + 30100 |
[active#(x1)] | = | 0 |
[tt] | = | 20585 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + 0 |
proper(isNePal(X)) | → | isNePal(proper(X)) | (18) |
active(and(tt,X)) | → | mark(X) | (4) |
proper(nil) | → | ok(nil) | (15) |
active(and(X1,X2)) | → | and(active(X1),X2) | (8) |
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(nil,X)) | → | mark(X) | (3) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (16) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (21) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (19) |
proper(tt) | → | ok(tt) | (17) |
active(isNePal(__(I,__(P,I)))) | → | mark(tt) | (5) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (10) |
active(__(X1,X2)) | → | __(X1,active(X2)) | (7) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (20) |
proper(__(X1,X2)) | → | __(proper(X1),proper(X2)) | (14) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (12) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (11) |
active(isNePal(X)) | → | isNePal(active(X)) | (9) |
isNePal(mark(X)) | → | mark(isNePal(X)) | (13) |
active(__(X1,X2)) | → | __(active(X1),X2) | (6) |
active(__(X,nil)) | → | mark(X) | (2) |
top#(ok(X)) | → | top#(active(X)) | (36) |
The dependency pairs are split into 0 components.
proper#(__(X1,X2)) | → | proper#(X2) | (32) |
proper#(and(X1,X2)) | → | proper#(X2) | (31) |
proper#(__(X1,X2)) | → | proper#(X1) | (29) |
proper#(and(X1,X2)) | → | proper#(X1) | (40) |
proper#(isNePal(X)) | → | proper#(X) | (25) |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 1 |
[proper(x1)] | = | 2 |
[ok(x1)] | = | x1 + 1 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | 0 |
[proper#(x1)] | = | x1 + 0 |
[active(x1)] | = | x1 + 1 |
[active#(x1)] | = | 0 |
[tt] | = | 0 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
active(and(tt,X)) | → | mark(X) | (4) |
proper(nil) | → | ok(nil) | (15) |
active(and(X1,X2)) | → | and(active(X1),X2) | (8) |
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(nil,X)) | → | mark(X) | (3) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (21) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (19) |
proper(tt) | → | ok(tt) | (17) |
active(isNePal(__(I,__(P,I)))) | → | mark(tt) | (5) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (10) |
active(__(X1,X2)) | → | __(X1,active(X2)) | (7) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (20) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (12) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (11) |
active(isNePal(X)) | → | isNePal(active(X)) | (9) |
isNePal(mark(X)) | → | mark(isNePal(X)) | (13) |
active(__(X1,X2)) | → | __(active(X1),X2) | (6) |
active(__(X,nil)) | → | mark(X) | (2) |
proper#(__(X1,X2)) | → | proper#(X2) | (32) |
proper#(and(X1,X2)) | → | proper#(X2) | (31) |
proper#(__(X1,X2)) | → | proper#(X1) | (29) |
proper#(and(X1,X2)) | → | proper#(X1) | (40) |
proper#(isNePal(X)) | → | proper#(X) | (25) |
The dependency pairs are split into 0 components.
active#(__(X1,X2)) | → | active#(X2) | (50) |
active#(and(X1,X2)) | → | active#(X1) | (41) |
active#(isNePal(X)) | → | active#(X) | (38) |
active#(__(X1,X2)) | → | active#(X1) | (24) |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 1 |
[proper(x1)] | = | 2 |
[ok(x1)] | = | x1 + 1 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[active#(x1)] | = | x1 + 0 |
[tt] | = | 0 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
active(and(tt,X)) | → | mark(X) | (4) |
proper(nil) | → | ok(nil) | (15) |
active(and(X1,X2)) | → | and(active(X1),X2) | (8) |
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(nil,X)) | → | mark(X) | (3) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (21) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (19) |
proper(tt) | → | ok(tt) | (17) |
active(isNePal(__(I,__(P,I)))) | → | mark(tt) | (5) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (10) |
active(__(X1,X2)) | → | __(X1,active(X2)) | (7) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (20) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (12) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (11) |
active(isNePal(X)) | → | isNePal(active(X)) | (9) |
isNePal(mark(X)) | → | mark(isNePal(X)) | (13) |
active(__(X1,X2)) | → | __(active(X1),X2) | (6) |
active(__(X,nil)) | → | mark(X) | (2) |
active#(__(X1,X2)) | → | active#(X2) | (50) |
active#(and(X1,X2)) | → | active#(X1) | (41) |
active#(isNePal(X)) | → | active#(X) | (38) |
active#(__(X1,X2)) | → | active#(X1) | (24) |
The dependency pairs are split into 0 components.
__#(mark(X1),X2) | → | __#(X1,X2) | (46) |
__#(ok(X1),ok(X2)) | → | __#(X1,X2) | (43) |
__#(X1,mark(X2)) | → | __#(X1,X2) | (26) |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 9508 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | x1 + x2 + 0 |
[isNePal(x1)] | = | x1 + 1 |
[proper(x1)] | = | 2 |
[ok(x1)] | = | x1 + 1 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[proper#(x1)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[active#(x1)] | = | 0 |
[tt] | = | 0 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
active(and(tt,X)) | → | mark(X) | (4) |
proper(nil) | → | ok(nil) | (15) |
active(and(X1,X2)) | → | and(active(X1),X2) | (8) |
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(nil,X)) | → | mark(X) | (3) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (21) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (19) |
proper(tt) | → | ok(tt) | (17) |
active(isNePal(__(I,__(P,I)))) | → | mark(tt) | (5) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (10) |
active(__(X1,X2)) | → | __(X1,active(X2)) | (7) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (20) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (12) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (11) |
active(isNePal(X)) | → | isNePal(active(X)) | (9) |
isNePal(mark(X)) | → | mark(isNePal(X)) | (13) |
active(__(X1,X2)) | → | __(active(X1),X2) | (6) |
active(__(X,nil)) | → | mark(X) | (2) |
__#(mark(X1),X2) | → | __#(X1,X2) | (46) |
__#(ok(X1),ok(X2)) | → | __#(X1,X2) | (43) |
__#(X1,mark(X2)) | → | __#(X1,X2) | (26) |
The dependency pairs are split into 0 components.
and#(mark(X1),X2) | → | and#(X1,X2) | (28) |
and#(ok(X1),ok(X2)) | → | and#(X1,X2) | (27) |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 17897 |
[proper(x1)] | = | 2 |
[ok(x1)] | = | x1 + 1 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[proper#(x1)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[active#(x1)] | = | 0 |
[tt] | = | 0 |
[and#(x1, x2)] | = | x2 + 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
active(and(tt,X)) | → | mark(X) | (4) |
proper(nil) | → | ok(nil) | (15) |
active(and(X1,X2)) | → | and(active(X1),X2) | (8) |
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(nil,X)) | → | mark(X) | (3) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (21) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (19) |
proper(tt) | → | ok(tt) | (17) |
active(isNePal(__(I,__(P,I)))) | → | mark(tt) | (5) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (10) |
active(__(X1,X2)) | → | __(X1,active(X2)) | (7) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (20) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (12) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (11) |
active(isNePal(X)) | → | isNePal(active(X)) | (9) |
isNePal(mark(X)) | → | mark(isNePal(X)) | (13) |
active(__(X1,X2)) | → | __(active(X1),X2) | (6) |
active(__(X,nil)) | → | mark(X) | (2) |
and#(ok(X1),ok(X2)) | → | and#(X1,X2) | (27) |
The dependency pairs are split into 1 component.
and#(mark(X1),X2) | → | and#(X1,X2) | (28) |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 34678 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 32024 |
[proper(x1)] | = | 2 |
[ok(x1)] | = | x1 + 1 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[proper#(x1)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[active#(x1)] | = | 0 |
[tt] | = | 0 |
[and#(x1, x2)] | = | x1 + 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
active(and(tt,X)) | → | mark(X) | (4) |
proper(nil) | → | ok(nil) | (15) |
active(and(X1,X2)) | → | and(active(X1),X2) | (8) |
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(nil,X)) | → | mark(X) | (3) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (21) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (19) |
proper(tt) | → | ok(tt) | (17) |
active(isNePal(__(I,__(P,I)))) | → | mark(tt) | (5) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (10) |
active(__(X1,X2)) | → | __(X1,active(X2)) | (7) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (20) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (12) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (11) |
active(isNePal(X)) | → | isNePal(active(X)) | (9) |
isNePal(mark(X)) | → | mark(isNePal(X)) | (13) |
active(__(X1,X2)) | → | __(active(X1),X2) | (6) |
active(__(X,nil)) | → | mark(X) | (2) |
and#(mark(X1),X2) | → | and#(X1,X2) | (28) |
The dependency pairs are split into 0 components.
isNePal#(mark(X)) | → | isNePal#(X) | (47) |
isNePal#(ok(X)) | → | isNePal#(X) | (35) |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 4426 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 1 |
[proper(x1)] | = | 2 |
[ok(x1)] | = | x1 + 1 |
[isNePal#(x1)] | = | x1 + 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[proper#(x1)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[active#(x1)] | = | 0 |
[tt] | = | 0 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
active(and(tt,X)) | → | mark(X) | (4) |
proper(nil) | → | ok(nil) | (15) |
active(and(X1,X2)) | → | and(active(X1),X2) | (8) |
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(nil,X)) | → | mark(X) | (3) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (21) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (19) |
proper(tt) | → | ok(tt) | (17) |
active(isNePal(__(I,__(P,I)))) | → | mark(tt) | (5) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (10) |
active(__(X1,X2)) | → | __(X1,active(X2)) | (7) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (20) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (12) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (11) |
active(isNePal(X)) | → | isNePal(active(X)) | (9) |
isNePal(mark(X)) | → | mark(isNePal(X)) | (13) |
active(__(X1,X2)) | → | __(active(X1),X2) | (6) |
active(__(X,nil)) | → | mark(X) | (2) |
isNePal#(mark(X)) | → | isNePal#(X) | (47) |
isNePal#(ok(X)) | → | isNePal#(X) | (35) |
The dependency pairs are split into 0 components.