The rewrite relation of the following TRS is considered.
active(zeros) | → | mark(cons(0,zeros)) | (1) |
active(U11(tt,L)) | → | mark(s(length(L))) | (2) |
active(and(tt,X)) | → | mark(X) | (3) |
active(isNat(0)) | → | mark(tt) | (4) |
active(isNat(length(V1))) | → | mark(isNatList(V1)) | (5) |
active(isNat(s(V1))) | → | mark(isNat(V1)) | (6) |
active(isNatIList(V)) | → | mark(isNatList(V)) | (7) |
active(isNatIList(zeros)) | → | mark(tt) | (8) |
active(isNatIList(cons(V1,V2))) | → | mark(and(isNat(V1),isNatIList(V2))) | (9) |
active(isNatList(nil)) | → | mark(tt) | (10) |
active(isNatList(cons(V1,V2))) | → | mark(and(isNat(V1),isNatList(V2))) | (11) |
active(length(nil)) | → | mark(0) | (12) |
active(length(cons(N,L))) | → | mark(U11(and(isNatList(L),isNat(N)),L)) | (13) |
mark(zeros) | → | active(zeros) | (14) |
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (15) |
mark(0) | → | active(0) | (16) |
mark(U11(X1,X2)) | → | active(U11(mark(X1),X2)) | (17) |
mark(tt) | → | active(tt) | (18) |
mark(s(X)) | → | active(s(mark(X))) | (19) |
mark(length(X)) | → | active(length(mark(X))) | (20) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (21) |
mark(isNat(X)) | → | active(isNat(X)) | (22) |
mark(isNatList(X)) | → | active(isNatList(X)) | (23) |
mark(isNatIList(X)) | → | active(isNatIList(X)) | (24) |
mark(nil) | → | active(nil) | (25) |
cons(mark(X1),X2) | → | cons(X1,X2) | (26) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (27) |
cons(active(X1),X2) | → | cons(X1,X2) | (28) |
cons(X1,active(X2)) | → | cons(X1,X2) | (29) |
U11(mark(X1),X2) | → | U11(X1,X2) | (30) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (31) |
U11(active(X1),X2) | → | U11(X1,X2) | (32) |
U11(X1,active(X2)) | → | U11(X1,X2) | (33) |
s(mark(X)) | → | s(X) | (34) |
s(active(X)) | → | s(X) | (35) |
length(mark(X)) | → | length(X) | (36) |
length(active(X)) | → | length(X) | (37) |
and(mark(X1),X2) | → | and(X1,X2) | (38) |
and(X1,mark(X2)) | → | and(X1,X2) | (39) |
and(active(X1),X2) | → | and(X1,X2) | (40) |
and(X1,active(X2)) | → | and(X1,X2) | (41) |
isNat(mark(X)) | → | isNat(X) | (42) |
isNat(active(X)) | → | isNat(X) | (43) |
isNatList(mark(X)) | → | isNatList(X) | (44) |
isNatList(active(X)) | → | isNatList(X) | (45) |
isNatIList(mark(X)) | → | isNatIList(X) | (46) |
isNatIList(active(X)) | → | isNatIList(X) | (47) |
[active(x1)] | = | 1 · x1 |
[zeros] | = | 0 |
[mark(x1)] | = | 1 · x1 |
[cons(x1, x2)] | = | 2 · x1 + 2 · x2 |
[0] | = | 0 |
[U11(x1, x2)] | = | 1 · x1 + 2 · x2 |
[tt] | = | 0 |
[s(x1)] | = | 1 · x1 |
[length(x1)] | = | 2 · x1 |
[and(x1, x2)] | = | 2 · x1 + 2 · x2 |
[isNat(x1)] | = | 1 · x1 |
[isNatList(x1)] | = | 1 · x1 |
[isNatIList(x1)] | = | 2 · x1 |
[nil] | = | 1 |
active(isNatList(nil)) | → | mark(tt) | (10) |
active(length(nil)) | → | mark(0) | (12) |
[active(x1)] | = | 1 · x1 |
[zeros] | = | 0 |
[mark(x1)] | = | 1 · x1 |
[cons(x1, x2)] | = | 2 · x1 + 2 · x2 |
[0] | = | 0 |
[U11(x1, x2)] | = | 1 · x1 + 2 · x2 |
[tt] | = | 0 |
[s(x1)] | = | 1 · x1 |
[length(x1)] | = | 2 · x1 |
[and(x1, x2)] | = | 1 · x1 + 1 · x2 |
[isNat(x1)] | = | 1 · x1 |
[isNatList(x1)] | = | 1 · x1 |
[isNatIList(x1)] | = | 1 + 1 · x1 |
[nil] | = | 0 |
active(isNatIList(V)) | → | mark(isNatList(V)) | (7) |
active(isNatIList(zeros)) | → | mark(tt) | (8) |
[active(x1)] | = | 1 · x1 |
[zeros] | = | 0 |
[mark(x1)] | = | 1 · x1 |
[cons(x1, x2)] | = | 2 · x1 + 2 · x2 |
[0] | = | 0 |
[U11(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[tt] | = | 0 |
[s(x1)] | = | 1 · x1 |
[length(x1)] | = | 2 + 2 · x1 |
[and(x1, x2)] | = | 1 · x1 + 1 · x2 |
[isNat(x1)] | = | 2 · x1 |
[isNatList(x1)] | = | 1 · x1 |
[isNatIList(x1)] | = | 1 · x1 |
[nil] | = | 0 |
active(isNat(length(V1))) | → | mark(isNatList(V1)) | (5) |
active#(zeros) | → | mark#(cons(0,zeros)) | (48) |
active#(zeros) | → | cons#(0,zeros) | (49) |
active#(U11(tt,L)) | → | mark#(s(length(L))) | (50) |
active#(U11(tt,L)) | → | s#(length(L)) | (51) |
active#(U11(tt,L)) | → | length#(L) | (52) |
active#(and(tt,X)) | → | mark#(X) | (53) |
active#(isNat(0)) | → | mark#(tt) | (54) |
active#(isNat(s(V1))) | → | mark#(isNat(V1)) | (55) |
active#(isNat(s(V1))) | → | isNat#(V1) | (56) |
active#(isNatIList(cons(V1,V2))) | → | mark#(and(isNat(V1),isNatIList(V2))) | (57) |
active#(isNatIList(cons(V1,V2))) | → | and#(isNat(V1),isNatIList(V2)) | (58) |
active#(isNatIList(cons(V1,V2))) | → | isNat#(V1) | (59) |
active#(isNatIList(cons(V1,V2))) | → | isNatIList#(V2) | (60) |
active#(isNatList(cons(V1,V2))) | → | mark#(and(isNat(V1),isNatList(V2))) | (61) |
active#(isNatList(cons(V1,V2))) | → | and#(isNat(V1),isNatList(V2)) | (62) |
active#(isNatList(cons(V1,V2))) | → | isNat#(V1) | (63) |
active#(isNatList(cons(V1,V2))) | → | isNatList#(V2) | (64) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
active#(length(cons(N,L))) | → | U11#(and(isNatList(L),isNat(N)),L) | (66) |
active#(length(cons(N,L))) | → | and#(isNatList(L),isNat(N)) | (67) |
active#(length(cons(N,L))) | → | isNatList#(L) | (68) |
active#(length(cons(N,L))) | → | isNat#(N) | (69) |
mark#(zeros) | → | active#(zeros) | (70) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (71) |
mark#(cons(X1,X2)) | → | cons#(mark(X1),X2) | (72) |
mark#(cons(X1,X2)) | → | mark#(X1) | (73) |
mark#(0) | → | active#(0) | (74) |
mark#(U11(X1,X2)) | → | active#(U11(mark(X1),X2)) | (75) |
mark#(U11(X1,X2)) | → | U11#(mark(X1),X2) | (76) |
mark#(U11(X1,X2)) | → | mark#(X1) | (77) |
mark#(tt) | → | active#(tt) | (78) |
mark#(s(X)) | → | active#(s(mark(X))) | (79) |
mark#(s(X)) | → | s#(mark(X)) | (80) |
mark#(s(X)) | → | mark#(X) | (81) |
mark#(length(X)) | → | active#(length(mark(X))) | (82) |
mark#(length(X)) | → | length#(mark(X)) | (83) |
mark#(length(X)) | → | mark#(X) | (84) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (85) |
mark#(and(X1,X2)) | → | and#(mark(X1),X2) | (86) |
mark#(and(X1,X2)) | → | mark#(X1) | (87) |
mark#(isNat(X)) | → | active#(isNat(X)) | (88) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (89) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (90) |
mark#(nil) | → | active#(nil) | (91) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (92) |
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (93) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (94) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (95) |
U11#(mark(X1),X2) | → | U11#(X1,X2) | (96) |
U11#(X1,mark(X2)) | → | U11#(X1,X2) | (97) |
U11#(active(X1),X2) | → | U11#(X1,X2) | (98) |
U11#(X1,active(X2)) | → | U11#(X1,X2) | (99) |
s#(mark(X)) | → | s#(X) | (100) |
s#(active(X)) | → | s#(X) | (101) |
length#(mark(X)) | → | length#(X) | (102) |
length#(active(X)) | → | length#(X) | (103) |
and#(mark(X1),X2) | → | and#(X1,X2) | (104) |
and#(X1,mark(X2)) | → | and#(X1,X2) | (105) |
and#(active(X1),X2) | → | and#(X1,X2) | (106) |
and#(X1,active(X2)) | → | and#(X1,X2) | (107) |
isNat#(mark(X)) | → | isNat#(X) | (108) |
isNat#(active(X)) | → | isNat#(X) | (109) |
isNatList#(mark(X)) | → | isNatList#(X) | (110) |
isNatList#(active(X)) | → | isNatList#(X) | (111) |
isNatIList#(mark(X)) | → | isNatIList#(X) | (112) |
isNatIList#(active(X)) | → | isNatIList#(X) | (113) |
The dependency pairs are split into 10 components.
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (71) |
active#(U11(tt,L)) | → | mark#(s(length(L))) | (50) |
mark#(s(X)) | → | active#(s(mark(X))) | (79) |
active#(and(tt,X)) | → | mark#(X) | (53) |
mark#(zeros) | → | active#(zeros) | (70) |
active#(zeros) | → | mark#(cons(0,zeros)) | (48) |
mark#(cons(X1,X2)) | → | mark#(X1) | (73) |
mark#(U11(X1,X2)) | → | active#(U11(mark(X1),X2)) | (75) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(U11(X1,X2)) | → | mark#(X1) | (77) |
mark#(s(X)) | → | mark#(X) | (81) |
mark#(length(X)) | → | active#(length(mark(X))) | (82) |
mark#(length(X)) | → | mark#(X) | (84) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (85) |
mark#(and(X1,X2)) | → | mark#(X1) | (87) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (89) |
active#(isNatList(cons(V1,V2))) | → | mark#(and(isNat(V1),isNatList(V2))) | (61) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (90) |
active#(isNatIList(cons(V1,V2))) | → | mark#(and(isNat(V1),isNatIList(V2))) | (57) |
We restrict the rewrite rules to the following usable rules of the DP problem.
mark(cons(X1,X2)) | → | active(cons(mark(X1),X2)) | (15) |
active(zeros) | → | mark(cons(0,zeros)) | (1) |
active(U11(tt,L)) | → | mark(s(length(L))) | (2) |
mark(s(X)) | → | active(s(mark(X))) | (19) |
active(and(tt,X)) | → | mark(X) | (3) |
mark(zeros) | → | active(zeros) | (14) |
mark(U11(X1,X2)) | → | active(U11(mark(X1),X2)) | (17) |
active(isNatIList(cons(V1,V2))) | → | mark(and(isNat(V1),isNatIList(V2))) | (9) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (21) |
active(isNatList(cons(V1,V2))) | → | mark(and(isNat(V1),isNatList(V2))) | (11) |
active(length(cons(N,L))) | → | mark(U11(and(isNatList(L),isNat(N)),L)) | (13) |
mark(length(X)) | → | active(length(mark(X))) | (20) |
mark(isNatList(X)) | → | active(isNatList(X)) | (23) |
mark(isNatIList(X)) | → | active(isNatIList(X)) | (24) |
mark(0) | → | active(0) | (16) |
mark(tt) | → | active(tt) | (18) |
active(isNat(s(V1))) | → | mark(isNat(V1)) | (6) |
mark(isNat(X)) | → | active(isNat(X)) | (22) |
mark(nil) | → | active(nil) | (25) |
and(X1,mark(X2)) | → | and(X1,X2) | (39) |
and(mark(X1),X2) | → | and(X1,X2) | (38) |
and(active(X1),X2) | → | and(X1,X2) | (40) |
and(X1,active(X2)) | → | and(X1,X2) | (41) |
active(isNat(0)) | → | mark(tt) | (4) |
cons(X1,mark(X2)) | → | cons(X1,X2) | (27) |
cons(mark(X1),X2) | → | cons(X1,X2) | (26) |
cons(active(X1),X2) | → | cons(X1,X2) | (28) |
cons(X1,active(X2)) | → | cons(X1,X2) | (29) |
s(active(X)) | → | s(X) | (35) |
s(mark(X)) | → | s(X) | (34) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (31) |
U11(mark(X1),X2) | → | U11(X1,X2) | (30) |
U11(active(X1),X2) | → | U11(X1,X2) | (32) |
U11(X1,active(X2)) | → | U11(X1,X2) | (33) |
length(active(X)) | → | length(X) | (37) |
length(mark(X)) | → | length(X) | (36) |
[mark(x1)] | = | 1 · x1 |
[cons(x1, x2)] | = | 1 · x1 + 2 · x2 |
[active(x1)] | = | 1 · x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[U11(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[tt] | = | 0 |
[s(x1)] | = | 1 · x1 |
[length(x1)] | = | 1 + 1 · x1 |
[and(x1, x2)] | = | 1 · x1 + 1 · x2 |
[isNatIList(x1)] | = | 1 · x1 |
[isNat(x1)] | = | 1 · x1 |
[isNatList(x1)] | = | 1 · x1 |
[nil] | = | 0 |
[mark#(x1)] | = | 2 · x1 |
[active#(x1)] | = | 2 · x1 |
mark#(U11(X1,X2)) | → | mark#(X1) | (77) |
mark#(length(X)) | → | mark#(X) | (84) |
isNat(mark(X)) | → | isNat(X) | (42) |
isNat(active(X)) | → | isNat(X) | (43) |
isNatList(mark(X)) | → | isNatList(X) | (44) |
isNatList(active(X)) | → | isNatList(X) | (45) |
isNatIList(mark(X)) | → | isNatIList(X) | (46) |
isNatIList(active(X)) | → | isNatIList(X) | (47) |
prec(mark#) | = | 3 | stat(mark#) | = | lex | |
prec(cons) | = | 0 | stat(cons) | = | lex | |
prec(mark) | = | 3 | stat(mark) | = | lex | |
prec(U11) | = | 3 | stat(U11) | = | lex | |
prec(tt) | = | 4 | stat(tt) | = | lex | |
prec(s) | = | 1 | stat(s) | = | lex | |
prec(length) | = | 3 | stat(length) | = | lex | |
prec(and) | = | 3 | stat(and) | = | lex | |
prec(zeros) | = | 3 | stat(zeros) | = | lex | |
prec(0) | = | 5 | stat(0) | = | lex | |
prec(isNatList) | = | 3 | stat(isNatList) | = | lex | |
prec(isNatIList) | = | 3 | stat(isNatIList) | = | lex | |
prec(active) | = | 3 | stat(active) | = | lex | |
prec(nil) | = | 2 | stat(nil) | = | lex |
π(mark#) | = | [] |
π(cons) | = | [] |
π(active#) | = | 1 |
π(mark) | = | [] |
π(U11) | = | [] |
π(tt) | = | [] |
π(s) | = | [] |
π(length) | = | [] |
π(and) | = | [] |
π(zeros) | = | [] |
π(0) | = | [] |
π(isNatList) | = | [] |
π(isNat) | = | 1 |
π(isNatIList) | = | [] |
π(active) | = | [] |
π(nil) | = | [] |
cons(X1,mark(X2)) | → | cons(X1,X2) | (27) |
cons(mark(X1),X2) | → | cons(X1,X2) | (26) |
cons(active(X1),X2) | → | cons(X1,X2) | (28) |
cons(X1,active(X2)) | → | cons(X1,X2) | (29) |
s(active(X)) | → | s(X) | (35) |
s(mark(X)) | → | s(X) | (34) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (31) |
U11(mark(X1),X2) | → | U11(X1,X2) | (30) |
U11(active(X1),X2) | → | U11(X1,X2) | (32) |
U11(X1,active(X2)) | → | U11(X1,X2) | (33) |
length(active(X)) | → | length(X) | (37) |
length(mark(X)) | → | length(X) | (36) |
and(X1,mark(X2)) | → | and(X1,X2) | (39) |
and(mark(X1),X2) | → | and(X1,X2) | (38) |
and(active(X1),X2) | → | and(X1,X2) | (40) |
and(X1,active(X2)) | → | and(X1,X2) | (41) |
mark#(cons(X1,X2)) | → | active#(cons(mark(X1),X2)) | (71) |
mark#(s(X)) | → | active#(s(mark(X))) | (79) |
[active#(x1)] | = | 2 + x1 |
[U11(x1, x2)] | = | -2 |
[and(x1, x2)] | = | x1 + x2 |
[length(x1)] | = | -2 |
[mark(x1)] | = | x1 |
[cons(x1, x2)] | = | 1 + x1 |
[active(x1)] | = | x1 |
[zeros] | = | 2 |
[0] | = | 0 |
[tt] | = | 0 |
[s(x1)] | = | x1 |
[isNatIList(x1)] | = | 0 |
[isNat(x1)] | = | 0 |
[isNatList(x1)] | = | 0 |
[nil] | = | 2 |
[mark#(x1)] | = | 2 + x1 |
active#(zeros) | → | mark#(cons(0,zeros)) | (48) |
mark#(cons(X1,X2)) | → | mark#(X1) | (73) |
The dependency pairs are split into 1 component.
mark#(s(X)) | → | mark#(X) | (81) |
mark#(U11(X1,X2)) | → | active#(U11(mark(X1),X2)) | (75) |
active#(U11(tt,L)) | → | mark#(s(length(L))) | (50) |
active#(and(tt,X)) | → | mark#(X) | (53) |
mark#(length(X)) | → | active#(length(mark(X))) | (82) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (85) |
mark#(and(X1,X2)) | → | mark#(X1) | (87) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (89) |
active#(isNatList(cons(V1,V2))) | → | mark#(and(isNat(V1),isNatList(V2))) | (61) |
mark#(isNatIList(X)) | → | active#(isNatIList(X)) | (90) |
active#(isNatIList(cons(V1,V2))) | → | mark#(and(isNat(V1),isNatIList(V2))) | (57) |
[mark#(x1)] | = |
|
||||||||||||
[s(x1)] | = |
|
||||||||||||
[U11(x1, x2)] | = |
|
||||||||||||
[active#(x1)] | = |
|
||||||||||||
[mark(x1)] | = |
|
||||||||||||
[tt] | = |
|
||||||||||||
[length(x1)] | = |
|
||||||||||||
[and(x1, x2)] | = |
|
||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||
[isNatList(x1)] | = |
|
||||||||||||
[isNat(x1)] | = |
|
||||||||||||
[isNatIList(x1)] | = |
|
||||||||||||
[active(x1)] | = |
|
||||||||||||
[zeros] | = |
|
||||||||||||
[0] | = |
|
||||||||||||
[nil] | = |
|
mark#(and(X1,X2)) | → | mark#(X1) | (87) |
prec(mark#) | = | 3 | stat(mark#) | = | lex | |
prec(U11) | = | 2 | stat(U11) | = | lex | |
prec(active#) | = | 3 | stat(active#) | = | lex | |
prec(mark) | = | 1 | stat(mark) | = | lex | |
prec(tt) | = | 4 | stat(tt) | = | lex | |
prec(length) | = | 2 | stat(length) | = | lex | |
prec(cons) | = | 1 | stat(cons) | = | lex | |
prec(isNatList) | = | 3 | stat(isNatList) | = | lex | |
prec(isNat) | = | 1 | stat(isNat) | = | lex | |
prec(isNatIList) | = | 1 | stat(isNatIList) | = | lex | |
prec(zeros) | = | 1 | stat(zeros) | = | lex | |
prec(0) | = | 1 | stat(0) | = | lex | |
prec(nil) | = | 0 | stat(nil) | = | lex |
π(mark#) | = | [1] |
π(s) | = | 1 |
π(U11) | = | [] |
π(active#) | = | [1] |
π(mark) | = | [1] |
π(tt) | = | [] |
π(length) | = | [] |
π(and) | = | 2 |
π(cons) | = | [2] |
π(isNatList) | = | [] |
π(isNat) | = | [] |
π(isNatIList) | = | [1] |
π(active) | = | 1 |
π(zeros) | = | [] |
π(0) | = | [] |
π(nil) | = | [] |
U11(X1,mark(X2)) | → | U11(X1,X2) | (31) |
U11(mark(X1),X2) | → | U11(X1,X2) | (30) |
U11(active(X1),X2) | → | U11(X1,X2) | (32) |
U11(X1,active(X2)) | → | U11(X1,X2) | (33) |
length(active(X)) | → | length(X) | (37) |
length(mark(X)) | → | length(X) | (36) |
and(X1,mark(X2)) | → | and(X1,X2) | (39) |
and(mark(X1),X2) | → | and(X1,X2) | (38) |
and(active(X1),X2) | → | and(X1,X2) | (40) |
and(X1,active(X2)) | → | and(X1,X2) | (41) |
active#(isNatIList(cons(V1,V2))) | → | mark#(and(isNat(V1),isNatIList(V2))) | (57) |
The dependency pairs are split into 1 component.
mark#(U11(X1,X2)) | → | active#(U11(mark(X1),X2)) | (75) |
active#(U11(tt,L)) | → | mark#(s(length(L))) | (50) |
mark#(s(X)) | → | mark#(X) | (81) |
mark#(length(X)) | → | active#(length(mark(X))) | (82) |
active#(and(tt,X)) | → | mark#(X) | (53) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (85) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(isNatList(X)) | → | active#(isNatList(X)) | (89) |
active#(isNatList(cons(V1,V2))) | → | mark#(and(isNat(V1),isNatList(V2))) | (61) |
[active#(x1)] | = | -2 + 2 · x1 |
[U11(x1, x2)] | = | 0 |
[and(x1, x2)] | = | 1 + 2 · x2 |
[length(x1)] | = | -2 |
[mark(x1)] | = | 2 + 2 · x1 |
[cons(x1, x2)] | = | 2 + 2 · x2 |
[active(x1)] | = | 2 + x1 |
[zeros] | = | 2 |
[0] | = | 1 |
[tt] | = | 0 |
[s(x1)] | = | 1 + 2 · x1 |
[isNatIList(x1)] | = | 0 |
[isNat(x1)] | = | 1 + 2 · x1 |
[isNatList(x1)] | = | 1 + 2 · x1 |
[nil] | = | 2 |
[mark#(x1)] | = | -2 + 2 · x1 |
U11(X1,mark(X2)) | → | U11(X1,X2) | (31) |
U11(mark(X1),X2) | → | U11(X1,X2) | (30) |
U11(active(X1),X2) | → | U11(X1,X2) | (32) |
U11(X1,active(X2)) | → | U11(X1,X2) | (33) |
length(active(X)) | → | length(X) | (37) |
length(mark(X)) | → | length(X) | (36) |
and(X1,mark(X2)) | → | and(X1,X2) | (39) |
and(mark(X1),X2) | → | and(X1,X2) | (38) |
and(active(X1),X2) | → | and(X1,X2) | (40) |
and(X1,active(X2)) | → | and(X1,X2) | (41) |
active#(isNatList(cons(V1,V2))) | → | mark#(and(isNat(V1),isNatList(V2))) | (61) |
The dependency pairs are split into 1 component.
active#(U11(tt,L)) | → | mark#(s(length(L))) | (50) |
mark#(s(X)) | → | mark#(X) | (81) |
mark#(U11(X1,X2)) | → | active#(U11(mark(X1),X2)) | (75) |
active#(and(tt,X)) | → | mark#(X) | (53) |
mark#(length(X)) | → | active#(length(mark(X))) | (82) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (85) |
[active#(x1)] | = | -2 + x1 |
[U11(x1, x2)] | = | -2 |
[and(x1, x2)] | = | 2 + 2 · x2 |
[length(x1)] | = | -2 |
[mark(x1)] | = | 2 + x1 |
[cons(x1, x2)] | = | -2 + 2 · x1 |
[active(x1)] | = | 2 + 2 · x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[s(x1)] | = | 1 + 2 · x1 |
[isNatIList(x1)] | = | 2 |
[isNat(x1)] | = | 0 |
[isNatList(x1)] | = | 0 |
[nil] | = | 0 |
[mark#(x1)] | = | -1 + x1 |
U11(X1,mark(X2)) | → | U11(X1,X2) | (31) |
U11(mark(X1),X2) | → | U11(X1,X2) | (30) |
U11(active(X1),X2) | → | U11(X1,X2) | (32) |
U11(X1,active(X2)) | → | U11(X1,X2) | (33) |
length(active(X)) | → | length(X) | (37) |
length(mark(X)) | → | length(X) | (36) |
and(X1,mark(X2)) | → | and(X1,X2) | (39) |
and(mark(X1),X2) | → | and(X1,X2) | (38) |
and(active(X1),X2) | → | and(X1,X2) | (40) |
and(X1,active(X2)) | → | and(X1,X2) | (41) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (85) |
[active#(x1)] | = | -1 + x1 |
[U11(x1, x2)] | = | 0 |
[length(x1)] | = | 1 |
[mark(x1)] | = | 0 |
[cons(x1, x2)] | = | -2 + x1 |
[active(x1)] | = | 2 · x1 |
[zeros] | = | 0 |
[0] | = | 1 |
[tt] | = | 2 |
[s(x1)] | = | 1 |
[and(x1, x2)] | = | -2 + 2 · x1 |
[isNatIList(x1)] | = | 1 + x1 |
[isNat(x1)] | = | x1 |
[isNatList(x1)] | = | 1 + x1 |
[nil] | = | 1 |
[mark#(x1)] | = | -2 |
U11(X1,mark(X2)) | → | U11(X1,X2) | (31) |
U11(mark(X1),X2) | → | U11(X1,X2) | (30) |
U11(active(X1),X2) | → | U11(X1,X2) | (32) |
U11(X1,active(X2)) | → | U11(X1,X2) | (33) |
length(active(X)) | → | length(X) | (37) |
length(mark(X)) | → | length(X) | (36) |
active#(and(tt,X)) | → | mark#(X) | (53) |
mark#(U11(x0,x1)) | → | active#(U11(x0,x1)) | (114) |
mark#(U11(cons(x0,x1),y1)) | → | active#(U11(active(cons(mark(x0),x1)),y1)) | (115) |
mark#(U11(s(x0),y1)) | → | active#(U11(active(s(mark(x0))),y1)) | (116) |
mark#(U11(zeros,y1)) | → | active#(U11(active(zeros),y1)) | (117) |
mark#(U11(U11(x0,x1),y1)) | → | active#(U11(active(U11(mark(x0),x1)),y1)) | (118) |
mark#(U11(and(x0,x1),y1)) | → | active#(U11(active(and(mark(x0),x1)),y1)) | (119) |
mark#(U11(length(x0),y1)) | → | active#(U11(active(length(mark(x0))),y1)) | (120) |
mark#(U11(isNatList(x0),y1)) | → | active#(U11(active(isNatList(x0)),y1)) | (121) |
mark#(U11(isNatIList(x0),y1)) | → | active#(U11(active(isNatIList(x0)),y1)) | (122) |
mark#(U11(0,y1)) | → | active#(U11(active(0),y1)) | (123) |
mark#(U11(tt,y1)) | → | active#(U11(active(tt),y1)) | (124) |
mark#(U11(isNat(x0),y1)) | → | active#(U11(active(isNat(x0)),y1)) | (125) |
mark#(U11(nil,y1)) | → | active#(U11(active(nil),y1)) | (126) |
mark#(length(x0)) | → | active#(length(x0)) | (127) |
mark#(length(cons(x0,x1))) | → | active#(length(active(cons(mark(x0),x1)))) | (128) |
mark#(length(s(x0))) | → | active#(length(active(s(mark(x0))))) | (129) |
mark#(length(zeros)) | → | active#(length(active(zeros))) | (130) |
mark#(length(U11(x0,x1))) | → | active#(length(active(U11(mark(x0),x1)))) | (131) |
mark#(length(and(x0,x1))) | → | active#(length(active(and(mark(x0),x1)))) | (132) |
mark#(length(length(x0))) | → | active#(length(active(length(mark(x0))))) | (133) |
mark#(length(isNatList(x0))) | → | active#(length(active(isNatList(x0)))) | (134) |
mark#(length(isNatIList(x0))) | → | active#(length(active(isNatIList(x0)))) | (135) |
mark#(length(0)) | → | active#(length(active(0))) | (136) |
mark#(length(tt)) | → | active#(length(active(tt))) | (137) |
mark#(length(isNat(x0))) | → | active#(length(active(isNat(x0)))) | (138) |
mark#(length(nil)) | → | active#(length(active(nil))) | (139) |
→ |
The dependency pairs are split into 1 component.
mark#(s(X)) | → | mark#(X) | (81) |
mark#(U11(x0,x1)) | → | active#(U11(x0,x1)) | (114) |
active#(U11(tt,L)) | → | mark#(s(length(L))) | (50) |
mark#(U11(cons(x0,x1),y1)) | → | active#(U11(active(cons(mark(x0),x1)),y1)) | (115) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(U11(and(x0,x1),y1)) | → | active#(U11(active(and(mark(x0),x1)),y1)) | (119) |
mark#(U11(s(x0),y1)) | → | active#(U11(active(s(mark(x0))),y1)) | (116) |
mark#(U11(zeros,y1)) | → | active#(U11(active(zeros),y1)) | (117) |
mark#(U11(U11(x0,x1),y1)) | → | active#(U11(active(U11(mark(x0),x1)),y1)) | (118) |
mark#(U11(length(x0),y1)) | → | active#(U11(active(length(mark(x0))),y1)) | (120) |
mark#(U11(isNatList(x0),y1)) | → | active#(U11(active(isNatList(x0)),y1)) | (121) |
mark#(U11(isNatIList(x0),y1)) | → | active#(U11(active(isNatIList(x0)),y1)) | (122) |
mark#(U11(0,y1)) | → | active#(U11(active(0),y1)) | (123) |
mark#(U11(tt,y1)) | → | active#(U11(active(tt),y1)) | (124) |
mark#(U11(isNat(x0),y1)) | → | active#(U11(active(isNat(x0)),y1)) | (125) |
mark#(U11(nil,y1)) | → | active#(U11(active(nil),y1)) | (126) |
mark#(length(x0)) | → | active#(length(x0)) | (127) |
mark#(length(cons(x0,x1))) | → | active#(length(active(cons(mark(x0),x1)))) | (128) |
mark#(length(s(x0))) | → | active#(length(active(s(mark(x0))))) | (129) |
mark#(length(zeros)) | → | active#(length(active(zeros))) | (130) |
mark#(length(U11(x0,x1))) | → | active#(length(active(U11(mark(x0),x1)))) | (131) |
mark#(length(and(x0,x1))) | → | active#(length(active(and(mark(x0),x1)))) | (132) |
mark#(length(length(x0))) | → | active#(length(active(length(mark(x0))))) | (133) |
mark#(length(isNatList(x0))) | → | active#(length(active(isNatList(x0)))) | (134) |
mark#(length(isNatIList(x0))) | → | active#(length(active(isNatIList(x0)))) | (135) |
mark#(length(tt)) | → | active#(length(active(tt))) | (137) |
mark#(length(isNat(x0))) | → | active#(length(active(isNat(x0)))) | (138) |
mark#(length(nil)) | → | active#(length(active(nil))) | (139) |
→ |
The dependency pairs are split into 1 component.
mark#(s(X)) | → | mark#(X) | (81) |
mark#(U11(x0,x1)) | → | active#(U11(x0,x1)) | (114) |
active#(U11(tt,L)) | → | mark#(s(length(L))) | (50) |
mark#(U11(cons(x0,x1),y1)) | → | active#(U11(active(cons(mark(x0),x1)),y1)) | (115) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(U11(and(x0,x1),y1)) | → | active#(U11(active(and(mark(x0),x1)),y1)) | (119) |
mark#(U11(s(x0),y1)) | → | active#(U11(active(s(mark(x0))),y1)) | (116) |
mark#(U11(zeros,y1)) | → | active#(U11(active(zeros),y1)) | (117) |
mark#(U11(U11(x0,x1),y1)) | → | active#(U11(active(U11(mark(x0),x1)),y1)) | (118) |
mark#(U11(length(x0),y1)) | → | active#(U11(active(length(mark(x0))),y1)) | (120) |
mark#(U11(isNatList(x0),y1)) | → | active#(U11(active(isNatList(x0)),y1)) | (121) |
mark#(U11(isNatIList(x0),y1)) | → | active#(U11(active(isNatIList(x0)),y1)) | (122) |
mark#(U11(0,y1)) | → | active#(U11(active(0),y1)) | (123) |
mark#(U11(tt,y1)) | → | active#(U11(active(tt),y1)) | (124) |
mark#(U11(isNat(x0),y1)) | → | active#(U11(active(isNat(x0)),y1)) | (125) |
mark#(U11(nil,y1)) | → | active#(U11(active(nil),y1)) | (126) |
mark#(length(x0)) | → | active#(length(x0)) | (127) |
mark#(length(cons(x0,x1))) | → | active#(length(active(cons(mark(x0),x1)))) | (128) |
mark#(length(s(x0))) | → | active#(length(active(s(mark(x0))))) | (129) |
mark#(length(zeros)) | → | active#(length(active(zeros))) | (130) |
mark#(length(U11(x0,x1))) | → | active#(length(active(U11(mark(x0),x1)))) | (131) |
mark#(length(and(x0,x1))) | → | active#(length(active(and(mark(x0),x1)))) | (132) |
mark#(length(length(x0))) | → | active#(length(active(length(mark(x0))))) | (133) |
mark#(length(isNatList(x0))) | → | active#(length(active(isNatList(x0)))) | (134) |
mark#(length(isNatIList(x0))) | → | active#(length(active(isNatIList(x0)))) | (135) |
mark#(length(isNat(x0))) | → | active#(length(active(isNat(x0)))) | (138) |
mark#(length(nil)) | → | active#(length(active(nil))) | (139) |
→ |
The dependency pairs are split into 1 component.
mark#(s(X)) | → | mark#(X) | (81) |
mark#(U11(x0,x1)) | → | active#(U11(x0,x1)) | (114) |
active#(U11(tt,L)) | → | mark#(s(length(L))) | (50) |
mark#(U11(cons(x0,x1),y1)) | → | active#(U11(active(cons(mark(x0),x1)),y1)) | (115) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(U11(and(x0,x1),y1)) | → | active#(U11(active(and(mark(x0),x1)),y1)) | (119) |
mark#(U11(s(x0),y1)) | → | active#(U11(active(s(mark(x0))),y1)) | (116) |
mark#(U11(zeros,y1)) | → | active#(U11(active(zeros),y1)) | (117) |
mark#(U11(U11(x0,x1),y1)) | → | active#(U11(active(U11(mark(x0),x1)),y1)) | (118) |
mark#(U11(length(x0),y1)) | → | active#(U11(active(length(mark(x0))),y1)) | (120) |
mark#(U11(isNatList(x0),y1)) | → | active#(U11(active(isNatList(x0)),y1)) | (121) |
mark#(U11(isNatIList(x0),y1)) | → | active#(U11(active(isNatIList(x0)),y1)) | (122) |
mark#(U11(0,y1)) | → | active#(U11(active(0),y1)) | (123) |
mark#(U11(tt,y1)) | → | active#(U11(active(tt),y1)) | (124) |
mark#(U11(isNat(x0),y1)) | → | active#(U11(active(isNat(x0)),y1)) | (125) |
mark#(U11(nil,y1)) | → | active#(U11(active(nil),y1)) | (126) |
mark#(length(x0)) | → | active#(length(x0)) | (127) |
mark#(length(cons(x0,x1))) | → | active#(length(active(cons(mark(x0),x1)))) | (128) |
mark#(length(s(x0))) | → | active#(length(active(s(mark(x0))))) | (129) |
mark#(length(zeros)) | → | active#(length(active(zeros))) | (130) |
mark#(length(U11(x0,x1))) | → | active#(length(active(U11(mark(x0),x1)))) | (131) |
mark#(length(and(x0,x1))) | → | active#(length(active(and(mark(x0),x1)))) | (132) |
mark#(length(length(x0))) | → | active#(length(active(length(mark(x0))))) | (133) |
mark#(length(isNatList(x0))) | → | active#(length(active(isNatList(x0)))) | (134) |
mark#(length(isNatIList(x0))) | → | active#(length(active(isNatIList(x0)))) | (135) |
mark#(length(isNat(x0))) | → | active#(length(active(isNat(x0)))) | (138) |
mark#(s(s(y_0))) | → | mark#(s(y_0)) | (143) |
mark#(s(U11(y_0,y_1))) | → | mark#(U11(y_0,y_1)) | (144) |
mark#(s(U11(cons(y_0,y_1),y_2))) | → | mark#(U11(cons(y_0,y_1),y_2)) | (145) |
mark#(s(U11(s(y_0),y_1))) | → | mark#(U11(s(y_0),y_1)) | (146) |
mark#(s(U11(zeros,y_0))) | → | mark#(U11(zeros,y_0)) | (147) |
mark#(s(U11(U11(y_0,y_1),y_2))) | → | mark#(U11(U11(y_0,y_1),y_2)) | (148) |
mark#(s(U11(and(y_0,y_1),y_2))) | → | mark#(U11(and(y_0,y_1),y_2)) | (149) |
mark#(s(U11(length(y_0),y_1))) | → | mark#(U11(length(y_0),y_1)) | (150) |
mark#(s(U11(isNatList(y_0),y_1))) | → | mark#(U11(isNatList(y_0),y_1)) | (151) |
mark#(s(U11(isNatIList(y_0),y_1))) | → | mark#(U11(isNatIList(y_0),y_1)) | (152) |
mark#(s(U11(0,y_0))) | → | mark#(U11(0,y_0)) | (153) |
mark#(s(U11(tt,y_0))) | → | mark#(U11(tt,y_0)) | (154) |
mark#(s(U11(isNat(y_0),y_1))) | → | mark#(U11(isNat(y_0),y_1)) | (155) |
mark#(s(U11(nil,y_0))) | → | mark#(U11(nil,y_0)) | (156) |
mark#(s(length(y_0))) | → | mark#(length(y_0)) | (157) |
mark#(s(length(cons(y_0,y_1)))) | → | mark#(length(cons(y_0,y_1))) | (158) |
mark#(s(length(s(y_0)))) | → | mark#(length(s(y_0))) | (159) |
mark#(s(length(zeros))) | → | mark#(length(zeros)) | (160) |
mark#(s(length(U11(y_0,y_1)))) | → | mark#(length(U11(y_0,y_1))) | (161) |
mark#(s(length(and(y_0,y_1)))) | → | mark#(length(and(y_0,y_1))) | (162) |
mark#(s(length(length(y_0)))) | → | mark#(length(length(y_0))) | (163) |
mark#(s(length(isNatList(y_0)))) | → | mark#(length(isNatList(y_0))) | (164) |
mark#(s(length(isNatIList(y_0)))) | → | mark#(length(isNatIList(y_0))) | (165) |
mark#(s(length(isNat(y_0)))) | → | mark#(length(isNat(y_0))) | (166) |
The dependency pairs are split into 2 components.
mark#(s(s(y_0))) | → | mark#(s(y_0)) | (143) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
We restrict the innermost strategy to the following left hand sides.
s(mark(x0)) |
s(active(x0)) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
mark#(s(s(y_0))) | → | mark#(s(y_0)) | (143) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
active#(U11(tt,L)) | → | mark#(s(length(L))) | (50) |
mark#(s(length(y_0))) | → | mark#(length(y_0)) | (157) |
mark#(length(x0)) | → | active#(length(x0)) | (127) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(U11(x0,x1)) | → | active#(U11(x0,x1)) | (114) |
mark#(U11(and(x0,x1),y1)) | → | active#(U11(active(and(mark(x0),x1)),y1)) | (119) |
mark#(length(cons(x0,x1))) | → | active#(length(active(cons(mark(x0),x1)))) | (128) |
mark#(length(s(x0))) | → | active#(length(active(s(mark(x0))))) | (129) |
mark#(length(zeros)) | → | active#(length(active(zeros))) | (130) |
mark#(length(U11(x0,x1))) | → | active#(length(active(U11(mark(x0),x1)))) | (131) |
mark#(length(and(x0,x1))) | → | active#(length(active(and(mark(x0),x1)))) | (132) |
mark#(length(length(x0))) | → | active#(length(active(length(mark(x0))))) | (133) |
mark#(length(isNatList(x0))) | → | active#(length(active(isNatList(x0)))) | (134) |
mark#(length(isNatIList(x0))) | → | active#(length(active(isNatIList(x0)))) | (135) |
mark#(length(isNat(x0))) | → | active#(length(active(isNat(x0)))) | (138) |
mark#(s(length(cons(y_0,y_1)))) | → | mark#(length(cons(y_0,y_1))) | (158) |
mark#(s(length(s(y_0)))) | → | mark#(length(s(y_0))) | (159) |
mark#(s(length(zeros))) | → | mark#(length(zeros)) | (160) |
mark#(s(length(U11(y_0,y_1)))) | → | mark#(length(U11(y_0,y_1))) | (161) |
mark#(s(length(and(y_0,y_1)))) | → | mark#(length(and(y_0,y_1))) | (162) |
mark#(s(length(length(y_0)))) | → | mark#(length(length(y_0))) | (163) |
mark#(s(length(isNatList(y_0)))) | → | mark#(length(isNatList(y_0))) | (164) |
mark#(s(length(isNatIList(y_0)))) | → | mark#(length(isNatIList(y_0))) | (165) |
mark#(s(length(isNat(y_0)))) | → | mark#(length(isNat(y_0))) | (166) |
mark#(U11(and(isNatList(z1),isNat(z0)),z1)) | → | active#(U11(and(isNatList(z1),isNat(z0)),z1)) | (167) |
The dependency pairs are split into 1 component.
mark#(s(length(y_0))) | → | mark#(length(y_0)) | (157) |
mark#(length(x0)) | → | active#(length(x0)) | (127) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(U11(and(x0,x1),y1)) | → | active#(U11(active(and(mark(x0),x1)),y1)) | (119) |
active#(U11(tt,L)) | → | mark#(s(length(L))) | (50) |
mark#(s(length(cons(y_0,y_1)))) | → | mark#(length(cons(y_0,y_1))) | (158) |
mark#(length(cons(x0,x1))) | → | active#(length(active(cons(mark(x0),x1)))) | (128) |
mark#(s(length(s(y_0)))) | → | mark#(length(s(y_0))) | (159) |
mark#(length(s(x0))) | → | active#(length(active(s(mark(x0))))) | (129) |
mark#(s(length(zeros))) | → | mark#(length(zeros)) | (160) |
mark#(length(zeros)) | → | active#(length(active(zeros))) | (130) |
mark#(s(length(U11(y_0,y_1)))) | → | mark#(length(U11(y_0,y_1))) | (161) |
mark#(length(U11(x0,x1))) | → | active#(length(active(U11(mark(x0),x1)))) | (131) |
mark#(s(length(and(y_0,y_1)))) | → | mark#(length(and(y_0,y_1))) | (162) |
mark#(length(and(x0,x1))) | → | active#(length(active(and(mark(x0),x1)))) | (132) |
mark#(s(length(length(y_0)))) | → | mark#(length(length(y_0))) | (163) |
mark#(length(length(x0))) | → | active#(length(active(length(mark(x0))))) | (133) |
mark#(s(length(isNatList(y_0)))) | → | mark#(length(isNatList(y_0))) | (164) |
mark#(length(isNatList(x0))) | → | active#(length(active(isNatList(x0)))) | (134) |
mark#(s(length(isNatIList(y_0)))) | → | mark#(length(isNatIList(y_0))) | (165) |
mark#(length(isNatIList(x0))) | → | active#(length(active(isNatIList(x0)))) | (135) |
mark#(s(length(isNat(y_0)))) | → | mark#(length(isNat(y_0))) | (166) |
mark#(length(isNat(x0))) | → | active#(length(active(isNat(x0)))) | (138) |
mark#(U11(and(isNatList(z1),isNat(z0)),z1)) | → | active#(U11(active(and(mark(isNatList(z1)),isNat(z0))),z1)) | (168) |
mark#(length(cons(y_0,y_1))) | → | active#(length(cons(y_0,y_1))) | (169) |
mark#(s(length(cons(y_0,y_1)))) | → | mark#(length(cons(y_0,y_1))) | (158) |
mark#(s(length(s(y_0)))) | → | mark#(length(s(y_0))) | (159) |
mark#(s(length(zeros))) | → | mark#(length(zeros)) | (160) |
mark#(s(length(U11(y_0,y_1)))) | → | mark#(length(U11(y_0,y_1))) | (161) |
mark#(s(length(and(y_0,y_1)))) | → | mark#(length(and(y_0,y_1))) | (162) |
mark#(s(length(length(y_0)))) | → | mark#(length(length(y_0))) | (163) |
mark#(s(length(isNatList(y_0)))) | → | mark#(length(isNatList(y_0))) | (164) |
mark#(s(length(isNatIList(y_0)))) | → | mark#(length(isNatIList(y_0))) | (165) |
mark#(s(length(isNat(y_0)))) | → | mark#(length(isNat(y_0))) | (166) |
active#(U11(tt,cons(y_0,y_1))) | → | mark#(s(length(cons(y_0,y_1)))) | (170) |
active#(U11(tt,s(y_0))) | → | mark#(s(length(s(y_0)))) | (171) |
active#(U11(tt,zeros)) | → | mark#(s(length(zeros))) | (172) |
active#(U11(tt,U11(y_0,y_1))) | → | mark#(s(length(U11(y_0,y_1)))) | (173) |
active#(U11(tt,and(y_0,y_1))) | → | mark#(s(length(and(y_0,y_1)))) | (174) |
active#(U11(tt,length(y_0))) | → | mark#(s(length(length(y_0)))) | (175) |
active#(U11(tt,isNatList(y_0))) | → | mark#(s(length(isNatList(y_0)))) | (176) |
active#(U11(tt,isNatIList(y_0))) | → | mark#(s(length(isNatIList(y_0)))) | (177) |
active#(U11(tt,isNat(y_0))) | → | mark#(s(length(isNat(y_0)))) | (178) |
[active#(x1)] | = |
|
||||||||||||
[length(x1)] | = |
|
||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||
[mark#(x1)] | = |
|
||||||||||||
[U11(x1, x2)] | = |
|
||||||||||||
[and(x1, x2)] | = |
|
||||||||||||
[isNatList(x1)] | = |
|
||||||||||||
[isNat(x1)] | = |
|
||||||||||||
[s(x1)] | = |
|
||||||||||||
[active(x1)] | = |
|
||||||||||||
[mark(x1)] | = |
|
||||||||||||
[zeros] | = |
|
||||||||||||
[isNatIList(x1)] | = |
|
||||||||||||
[tt] | = |
|
||||||||||||
[0] | = |
|
||||||||||||
[nil] | = |
|
active#(U11(tt,isNatIList(y_0))) | → | mark#(s(length(isNatIList(y_0)))) | (177) |
The dependency pairs are split into 1 component.
mark#(U11(and(isNatList(z1),isNat(z0)),z1)) | → | active#(U11(active(and(mark(isNatList(z1)),isNat(z0))),z1)) | (168) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
active#(U11(tt,cons(y_0,y_1))) | → | mark#(s(length(cons(y_0,y_1)))) | (170) |
mark#(s(length(cons(y_0,y_1)))) | → | mark#(length(cons(y_0,y_1))) | (158) |
mark#(length(cons(x0,x1))) | → | active#(length(active(cons(mark(x0),x1)))) | (128) |
active#(U11(tt,s(y_0))) | → | mark#(s(length(s(y_0)))) | (171) |
mark#(s(length(s(y_0)))) | → | mark#(length(s(y_0))) | (159) |
mark#(length(s(x0))) | → | active#(length(active(s(mark(x0))))) | (129) |
active#(U11(tt,zeros)) | → | mark#(s(length(zeros))) | (172) |
mark#(s(length(zeros))) | → | mark#(length(zeros)) | (160) |
mark#(length(zeros)) | → | active#(length(active(zeros))) | (130) |
active#(U11(tt,U11(y_0,y_1))) | → | mark#(s(length(U11(y_0,y_1)))) | (173) |
mark#(s(length(U11(y_0,y_1)))) | → | mark#(length(U11(y_0,y_1))) | (161) |
mark#(length(U11(x0,x1))) | → | active#(length(active(U11(mark(x0),x1)))) | (131) |
active#(U11(tt,and(y_0,y_1))) | → | mark#(s(length(and(y_0,y_1)))) | (174) |
mark#(s(length(and(y_0,y_1)))) | → | mark#(length(and(y_0,y_1))) | (162) |
mark#(length(and(x0,x1))) | → | active#(length(active(and(mark(x0),x1)))) | (132) |
active#(U11(tt,length(y_0))) | → | mark#(s(length(length(y_0)))) | (175) |
mark#(s(length(length(y_0)))) | → | mark#(length(length(y_0))) | (163) |
mark#(length(length(x0))) | → | active#(length(active(length(mark(x0))))) | (133) |
active#(U11(tt,isNatList(y_0))) | → | mark#(s(length(isNatList(y_0)))) | (176) |
mark#(s(length(isNatList(y_0)))) | → | mark#(length(isNatList(y_0))) | (164) |
mark#(length(isNatList(x0))) | → | active#(length(active(isNatList(x0)))) | (134) |
active#(U11(tt,isNat(y_0))) | → | mark#(s(length(isNat(y_0)))) | (178) |
mark#(s(length(isNat(y_0)))) | → | mark#(length(isNat(y_0))) | (166) |
mark#(length(isNat(x0))) | → | active#(length(active(isNat(x0)))) | (138) |
mark#(length(cons(y_0,y_1))) | → | active#(length(cons(y_0,y_1))) | (169) |
[active#(x1)] | = | 2 · x1 |
[U11(x1, x2)] | = | 2 · x2 |
[length(x1)] | = | x1 |
[mark(x1)] | = | x1 |
[cons(x1, x2)] | = | 2 · x2 |
[active(x1)] | = | x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[s(x1)] | = | 2 · x1 |
[and(x1, x2)] | = | 2 · x2 |
[isNatIList(x1)] | = | 0 |
[isNat(x1)] | = | 2 |
[isNatList(x1)] | = | 0 |
[nil] | = | 2 |
[mark#(x1)] | = | 2 · x1 |
mark#(s(length(isNat(y_0)))) | → | mark#(length(isNat(y_0))) | (166) |
The dependency pairs are split into 1 component.
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(U11(and(isNatList(z1),isNat(z0)),z1)) | → | active#(U11(active(and(mark(isNatList(z1)),isNat(z0))),z1)) | (168) |
active#(U11(tt,cons(y_0,y_1))) | → | mark#(s(length(cons(y_0,y_1)))) | (170) |
mark#(s(length(cons(y_0,y_1)))) | → | mark#(length(cons(y_0,y_1))) | (158) |
mark#(length(cons(x0,x1))) | → | active#(length(active(cons(mark(x0),x1)))) | (128) |
active#(U11(tt,s(y_0))) | → | mark#(s(length(s(y_0)))) | (171) |
mark#(s(length(s(y_0)))) | → | mark#(length(s(y_0))) | (159) |
mark#(length(s(x0))) | → | active#(length(active(s(mark(x0))))) | (129) |
active#(U11(tt,zeros)) | → | mark#(s(length(zeros))) | (172) |
mark#(s(length(zeros))) | → | mark#(length(zeros)) | (160) |
mark#(length(zeros)) | → | active#(length(active(zeros))) | (130) |
active#(U11(tt,U11(y_0,y_1))) | → | mark#(s(length(U11(y_0,y_1)))) | (173) |
mark#(s(length(U11(y_0,y_1)))) | → | mark#(length(U11(y_0,y_1))) | (161) |
mark#(length(U11(x0,x1))) | → | active#(length(active(U11(mark(x0),x1)))) | (131) |
active#(U11(tt,and(y_0,y_1))) | → | mark#(s(length(and(y_0,y_1)))) | (174) |
mark#(s(length(and(y_0,y_1)))) | → | mark#(length(and(y_0,y_1))) | (162) |
mark#(length(and(x0,x1))) | → | active#(length(active(and(mark(x0),x1)))) | (132) |
active#(U11(tt,length(y_0))) | → | mark#(s(length(length(y_0)))) | (175) |
mark#(s(length(length(y_0)))) | → | mark#(length(length(y_0))) | (163) |
mark#(length(length(x0))) | → | active#(length(active(length(mark(x0))))) | (133) |
active#(U11(tt,isNatList(y_0))) | → | mark#(s(length(isNatList(y_0)))) | (176) |
mark#(s(length(isNatList(y_0)))) | → | mark#(length(isNatList(y_0))) | (164) |
mark#(length(isNatList(x0))) | → | active#(length(active(isNatList(x0)))) | (134) |
mark#(length(cons(y_0,y_1))) | → | active#(length(cons(y_0,y_1))) | (169) |
[active#(x1)] | = | -2 + 2 · x1 |
[U11(x1, x2)] | = | 2 + 2 · x2 |
[length(x1)] | = | 2 + x1 |
[mark(x1)] | = | x1 |
[cons(x1, x2)] | = | 2 · x2 |
[active(x1)] | = | x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[s(x1)] | = | x1 |
[and(x1, x2)] | = | 2 · x2 |
[isNatIList(x1)] | = | 0 |
[isNat(x1)] | = | 0 |
[isNatList(x1)] | = | 2 · x1 |
[nil] | = | 2 |
[mark#(x1)] | = | -2 + 2 · x1 |
active#(U11(tt,U11(y_0,y_1))) | → | mark#(s(length(U11(y_0,y_1)))) | (173) |
active#(U11(tt,length(y_0))) | → | mark#(s(length(length(y_0)))) | (175) |
The dependency pairs are split into 1 component.
mark#(U11(and(isNatList(z1),isNat(z0)),z1)) | → | active#(U11(active(and(mark(isNatList(z1)),isNat(z0))),z1)) | (168) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
active#(U11(tt,cons(y_0,y_1))) | → | mark#(s(length(cons(y_0,y_1)))) | (170) |
mark#(s(length(cons(y_0,y_1)))) | → | mark#(length(cons(y_0,y_1))) | (158) |
mark#(length(cons(x0,x1))) | → | active#(length(active(cons(mark(x0),x1)))) | (128) |
active#(U11(tt,s(y_0))) | → | mark#(s(length(s(y_0)))) | (171) |
mark#(s(length(s(y_0)))) | → | mark#(length(s(y_0))) | (159) |
mark#(length(s(x0))) | → | active#(length(active(s(mark(x0))))) | (129) |
active#(U11(tt,zeros)) | → | mark#(s(length(zeros))) | (172) |
mark#(s(length(zeros))) | → | mark#(length(zeros)) | (160) |
mark#(length(zeros)) | → | active#(length(active(zeros))) | (130) |
active#(U11(tt,and(y_0,y_1))) | → | mark#(s(length(and(y_0,y_1)))) | (174) |
mark#(s(length(and(y_0,y_1)))) | → | mark#(length(and(y_0,y_1))) | (162) |
mark#(length(and(x0,x1))) | → | active#(length(active(and(mark(x0),x1)))) | (132) |
active#(U11(tt,isNatList(y_0))) | → | mark#(s(length(isNatList(y_0)))) | (176) |
mark#(s(length(isNatList(y_0)))) | → | mark#(length(isNatList(y_0))) | (164) |
mark#(length(isNatList(x0))) | → | active#(length(active(isNatList(x0)))) | (134) |
mark#(length(cons(y_0,y_1))) | → | active#(length(cons(y_0,y_1))) | (169) |
[active#(x1)] | = | -2 + 2 · x1 |
[U11(x1, x2)] | = | 2 + 2 · x2 |
[length(x1)] | = | 2 + x1 |
[mark(x1)] | = | x1 |
[cons(x1, x2)] | = | 2 · x2 |
[active(x1)] | = | x1 |
[zeros] | = | 0 |
[0] | = | 0 |
[tt] | = | 0 |
[s(x1)] | = | x1 |
[and(x1, x2)] | = | x2 |
[isNatIList(x1)] | = | 0 |
[isNat(x1)] | = | 0 |
[isNatList(x1)] | = | 1 |
[nil] | = | 2 |
[mark#(x1)] | = | -2 + 2 · x1 |
active#(U11(tt,isNatList(y_0))) | → | mark#(s(length(isNatList(y_0)))) | (176) |
The dependency pairs are split into 1 component.
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(U11(and(isNatList(z1),isNat(z0)),z1)) | → | active#(U11(active(and(mark(isNatList(z1)),isNat(z0))),z1)) | (168) |
active#(U11(tt,cons(y_0,y_1))) | → | mark#(s(length(cons(y_0,y_1)))) | (170) |
mark#(s(length(cons(y_0,y_1)))) | → | mark#(length(cons(y_0,y_1))) | (158) |
mark#(length(cons(x0,x1))) | → | active#(length(active(cons(mark(x0),x1)))) | (128) |
active#(U11(tt,s(y_0))) | → | mark#(s(length(s(y_0)))) | (171) |
mark#(s(length(s(y_0)))) | → | mark#(length(s(y_0))) | (159) |
mark#(length(s(x0))) | → | active#(length(active(s(mark(x0))))) | (129) |
active#(U11(tt,zeros)) | → | mark#(s(length(zeros))) | (172) |
mark#(s(length(zeros))) | → | mark#(length(zeros)) | (160) |
mark#(length(zeros)) | → | active#(length(active(zeros))) | (130) |
active#(U11(tt,and(y_0,y_1))) | → | mark#(s(length(and(y_0,y_1)))) | (174) |
mark#(s(length(and(y_0,y_1)))) | → | mark#(length(and(y_0,y_1))) | (162) |
mark#(length(and(x0,x1))) | → | active#(length(active(and(mark(x0),x1)))) | (132) |
mark#(length(cons(y_0,y_1))) | → | active#(length(cons(y_0,y_1))) | (169) |
[active#(x1)] | = |
|
||||||||||||
[length(x1)] | = |
|
||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||
[mark#(x1)] | = |
|
||||||||||||
[U11(x1, x2)] | = |
|
||||||||||||
[and(x1, x2)] | = |
|
||||||||||||
[isNatList(x1)] | = |
|
||||||||||||
[isNat(x1)] | = |
|
||||||||||||
[active(x1)] | = |
|
||||||||||||
[mark(x1)] | = |
|
||||||||||||
[tt] | = |
|
||||||||||||
[s(x1)] | = |
|
||||||||||||
[zeros] | = |
|
||||||||||||
[0] | = |
|
||||||||||||
[isNatIList(x1)] | = |
|
||||||||||||
[nil] | = |
|
active#(U11(tt,cons(y_0,y_1))) | → | mark#(s(length(cons(y_0,y_1)))) | (170) |
The dependency pairs are split into 1 component.
mark#(U11(and(isNatList(z1),isNat(z0)),z1)) | → | active#(U11(active(and(mark(isNatList(z1)),isNat(z0))),z1)) | (168) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
active#(U11(tt,s(y_0))) | → | mark#(s(length(s(y_0)))) | (171) |
mark#(s(length(s(y_0)))) | → | mark#(length(s(y_0))) | (159) |
mark#(length(s(x0))) | → | active#(length(active(s(mark(x0))))) | (129) |
active#(U11(tt,zeros)) | → | mark#(s(length(zeros))) | (172) |
mark#(s(length(zeros))) | → | mark#(length(zeros)) | (160) |
mark#(length(zeros)) | → | active#(length(active(zeros))) | (130) |
active#(U11(tt,and(y_0,y_1))) | → | mark#(s(length(and(y_0,y_1)))) | (174) |
mark#(s(length(and(y_0,y_1)))) | → | mark#(length(and(y_0,y_1))) | (162) |
mark#(length(and(x0,x1))) | → | active#(length(active(and(mark(x0),x1)))) | (132) |
[mark#(x1)] | = |
|
||||||||||||
[U11(x1, x2)] | = |
|
||||||||||||
[and(x1, x2)] | = |
|
||||||||||||
[isNatList(x1)] | = |
|
||||||||||||
[isNat(x1)] | = |
|
||||||||||||
[active#(x1)] | = |
|
||||||||||||
[active(x1)] | = |
|
||||||||||||
[mark(x1)] | = |
|
||||||||||||
[length(x1)] | = |
|
||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||
[tt] | = |
|
||||||||||||
[s(x1)] | = |
|
||||||||||||
[zeros] | = |
|
||||||||||||
[0] | = |
|
||||||||||||
[isNatIList(x1)] | = |
|
||||||||||||
[nil] | = |
|
active#(U11(tt,and(y_0,y_1))) | → | mark#(s(length(and(y_0,y_1)))) | (174) |
The dependency pairs are split into 1 component.
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(U11(and(isNatList(z1),isNat(z0)),z1)) | → | active#(U11(active(and(mark(isNatList(z1)),isNat(z0))),z1)) | (168) |
active#(U11(tt,s(y_0))) | → | mark#(s(length(s(y_0)))) | (171) |
mark#(s(length(s(y_0)))) | → | mark#(length(s(y_0))) | (159) |
mark#(length(s(x0))) | → | active#(length(active(s(mark(x0))))) | (129) |
active#(U11(tt,zeros)) | → | mark#(s(length(zeros))) | (172) |
mark#(s(length(zeros))) | → | mark#(length(zeros)) | (160) |
mark#(length(zeros)) | → | active#(length(active(zeros))) | (130) |
prec(cons) | = | 1 | stat(cons) | = | lex | |
prec(mark#) | = | 1 | stat(mark#) | = | lex | |
prec(U11) | = | 1 | stat(U11) | = | lex | |
prec(isNatList) | = | 2 | stat(isNatList) | = | lex | |
prec(isNat) | = | 3 | stat(isNat) | = | lex | |
prec(tt) | = | 3 | stat(tt) | = | lex | |
prec(s) | = | 0 | stat(s) | = | lex | |
prec(zeros) | = | 1 | stat(zeros) | = | lex | |
prec(0) | = | 4 | stat(0) | = | lex | |
prec(isNatIList) | = | 5 | stat(isNatIList) | = | lex | |
prec(nil) | = | 6 | stat(nil) | = | lex |
π(active#) | = | 1 |
π(length) | = | 1 |
π(cons) | = | [] |
π(mark#) | = | [] |
π(U11) | = | [] |
π(and) | = | 2 |
π(isNatList) | = | [] |
π(isNat) | = | [] |
π(active) | = | 1 |
π(mark) | = | 1 |
π(tt) | = | [] |
π(s) | = | [] |
π(zeros) | = | [] |
π(0) | = | [] |
π(isNatIList) | = | [] |
π(nil) | = | [] |
mark#(length(s(x0))) | → | active#(length(active(s(mark(x0))))) | (129) |
The dependency pairs are split into 1 component.
mark#(U11(and(isNatList(z1),isNat(z0)),z1)) | → | active#(U11(active(and(mark(isNatList(z1)),isNat(z0))),z1)) | (168) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
active#(U11(tt,zeros)) | → | mark#(s(length(zeros))) | (172) |
mark#(s(length(zeros))) | → | mark#(length(zeros)) | (160) |
mark#(length(zeros)) | → | active#(length(active(zeros))) | (130) |
[mark#(x1)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[U11(x1, x2)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[isNatList(x1)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[isNat(x1)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[active#(x1)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[length(x1)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[tt] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[zeros] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[0] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[isNatIList(x1)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||
[nil] | = |
|
mark#(s(length(zeros))) | → | mark#(length(zeros)) | (160) |
The dependency pairs are split into 1 component.
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(U11(and(isNatList(z1),isNat(z0)),z1)) | → | active#(U11(active(and(mark(isNatList(z1)),isNat(z0))),z1)) | (168) |
prec(length) | = | 2 | weight(length) | = | 1 | ||||
prec(mark#) | = | 1 | weight(mark#) | = | 1 | ||||
prec(U11) | = | 0 | weight(U11) | = | 1 |
π(active#) | = | 1 |
π(length) | = | [] |
π(mark#) | = | [] |
π(U11) | = | [] |
U11(X1,mark(X2)) | → | U11(X1,X2) | (31) |
U11(mark(X1),X2) | → | U11(X1,X2) | (30) |
U11(active(X1),X2) | → | U11(X1,X2) | (32) |
U11(X1,active(X2)) | → | U11(X1,X2) | (33) |
active#(length(cons(N,L))) | → | mark#(U11(and(isNatList(L),isNat(N)),L)) | (65) |
mark#(U11(and(isNatList(z1),isNat(z0)),z1)) | → | active#(U11(active(and(mark(isNatList(z1)),isNat(z0))),z1)) | (168) |
There are no pairs anymore.
active#(isNat(s(V1))) | → | mark#(isNat(V1)) | (55) |
mark#(isNat(X)) | → | active#(isNat(X)) | (88) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
We restrict the innermost strategy to the following left hand sides.
s(mark(x0)) |
s(active(x0)) |
isNat(mark(x0)) |
isNat(active(x0)) |
[active#(x1)] | = | 1 · x1 |
[isNat(x1)] | = | 2 · x1 |
[s(x1)] | = | 2 · x1 |
[mark#(x1)] | = | 2 · x1 |
active#(isNat(s(V1))) | → | mark#(isNat(V1)) | (55) |
We restrict the innermost strategy to the following left hand sides.
isNat(mark(x0)) |
isNat(active(x0)) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
mark#(isNat(X)) | → | active#(isNat(X)) | (88) |
1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
cons#(X1,mark(X2)) | → | cons#(X1,X2) | (93) |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (92) |
cons#(active(X1),X2) | → | cons#(X1,X2) | (94) |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (95) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
We restrict the innermost strategy to the following left hand sides.
active(zeros) |
active(U11(tt,x0)) |
active(and(tt,x0)) |
active(isNat(0)) |
active(isNat(length(x0))) |
active(isNat(s(x0))) |
active(isNatIList(x0)) |
active(isNatList(nil)) |
active(isNatList(cons(x0,x1))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(zeros) |
mark(cons(x0,x1)) |
mark(0) |
mark(U11(x0,x1)) |
mark(tt) |
mark(s(x0)) |
mark(length(x0)) |
mark(and(x0,x1)) |
mark(isNat(x0)) |
mark(isNatList(x0)) |
mark(isNatIList(x0)) |
mark(nil) |
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) | (93) |
1 | ≥ | 1 | |
2 | > | 2 | |
cons#(mark(X1),X2) | → | cons#(X1,X2) | (92) |
1 | > | 1 | |
2 | ≥ | 2 | |
cons#(active(X1),X2) | → | cons#(X1,X2) | (94) |
1 | > | 1 | |
2 | ≥ | 2 | |
cons#(X1,active(X2)) | → | cons#(X1,X2) | (95) |
1 | ≥ | 1 | |
2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
U11#(X1,mark(X2)) | → | U11#(X1,X2) | (97) |
U11#(mark(X1),X2) | → | U11#(X1,X2) | (96) |
U11#(active(X1),X2) | → | U11#(X1,X2) | (98) |
U11#(X1,active(X2)) | → | U11#(X1,X2) | (99) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
We restrict the innermost strategy to the following left hand sides.
active(zeros) |
active(U11(tt,x0)) |
active(and(tt,x0)) |
active(isNat(0)) |
active(isNat(length(x0))) |
active(isNat(s(x0))) |
active(isNatIList(x0)) |
active(isNatList(nil)) |
active(isNatList(cons(x0,x1))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(zeros) |
mark(cons(x0,x1)) |
mark(0) |
mark(U11(x0,x1)) |
mark(tt) |
mark(s(x0)) |
mark(length(x0)) |
mark(and(x0,x1)) |
mark(isNat(x0)) |
mark(isNatList(x0)) |
mark(isNatIList(x0)) |
mark(nil) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
U11#(X1,mark(X2)) | → | U11#(X1,X2) | (97) |
1 | ≥ | 1 | |
2 | > | 2 | |
U11#(mark(X1),X2) | → | U11#(X1,X2) | (96) |
1 | > | 1 | |
2 | ≥ | 2 | |
U11#(active(X1),X2) | → | U11#(X1,X2) | (98) |
1 | > | 1 | |
2 | ≥ | 2 | |
U11#(X1,active(X2)) | → | U11#(X1,X2) | (99) |
1 | ≥ | 1 | |
2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
s#(active(X)) | → | s#(X) | (101) |
s#(mark(X)) | → | s#(X) | (100) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
We restrict the innermost strategy to the following left hand sides.
active(zeros) |
active(U11(tt,x0)) |
active(and(tt,x0)) |
active(isNat(0)) |
active(isNat(length(x0))) |
active(isNat(s(x0))) |
active(isNatIList(x0)) |
active(isNatList(nil)) |
active(isNatList(cons(x0,x1))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(zeros) |
mark(cons(x0,x1)) |
mark(0) |
mark(U11(x0,x1)) |
mark(tt) |
mark(s(x0)) |
mark(length(x0)) |
mark(and(x0,x1)) |
mark(isNat(x0)) |
mark(isNatList(x0)) |
mark(isNatIList(x0)) |
mark(nil) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
s#(active(X)) | → | s#(X) | (101) |
1 | > | 1 | |
s#(mark(X)) | → | s#(X) | (100) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
length#(active(X)) | → | length#(X) | (103) |
length#(mark(X)) | → | length#(X) | (102) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
We restrict the innermost strategy to the following left hand sides.
active(zeros) |
active(U11(tt,x0)) |
active(and(tt,x0)) |
active(isNat(0)) |
active(isNat(length(x0))) |
active(isNat(s(x0))) |
active(isNatIList(x0)) |
active(isNatList(nil)) |
active(isNatList(cons(x0,x1))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(zeros) |
mark(cons(x0,x1)) |
mark(0) |
mark(U11(x0,x1)) |
mark(tt) |
mark(s(x0)) |
mark(length(x0)) |
mark(and(x0,x1)) |
mark(isNat(x0)) |
mark(isNatList(x0)) |
mark(isNatIList(x0)) |
mark(nil) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
length#(active(X)) | → | length#(X) | (103) |
1 | > | 1 | |
length#(mark(X)) | → | length#(X) | (102) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
and#(X1,mark(X2)) | → | and#(X1,X2) | (105) |
and#(mark(X1),X2) | → | and#(X1,X2) | (104) |
and#(active(X1),X2) | → | and#(X1,X2) | (106) |
and#(X1,active(X2)) | → | and#(X1,X2) | (107) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
We restrict the innermost strategy to the following left hand sides.
active(zeros) |
active(U11(tt,x0)) |
active(and(tt,x0)) |
active(isNat(0)) |
active(isNat(length(x0))) |
active(isNat(s(x0))) |
active(isNatIList(x0)) |
active(isNatList(nil)) |
active(isNatList(cons(x0,x1))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(zeros) |
mark(cons(x0,x1)) |
mark(0) |
mark(U11(x0,x1)) |
mark(tt) |
mark(s(x0)) |
mark(length(x0)) |
mark(and(x0,x1)) |
mark(isNat(x0)) |
mark(isNatList(x0)) |
mark(isNatIList(x0)) |
mark(nil) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
and#(X1,mark(X2)) | → | and#(X1,X2) | (105) |
1 | ≥ | 1 | |
2 | > | 2 | |
and#(mark(X1),X2) | → | and#(X1,X2) | (104) |
1 | > | 1 | |
2 | ≥ | 2 | |
and#(active(X1),X2) | → | and#(X1,X2) | (106) |
1 | > | 1 | |
2 | ≥ | 2 | |
and#(X1,active(X2)) | → | and#(X1,X2) | (107) |
1 | ≥ | 1 | |
2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
isNat#(active(X)) | → | isNat#(X) | (109) |
isNat#(mark(X)) | → | isNat#(X) | (108) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
We restrict the innermost strategy to the following left hand sides.
active(zeros) |
active(U11(tt,x0)) |
active(and(tt,x0)) |
active(isNat(0)) |
active(isNat(length(x0))) |
active(isNat(s(x0))) |
active(isNatIList(x0)) |
active(isNatList(nil)) |
active(isNatList(cons(x0,x1))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(zeros) |
mark(cons(x0,x1)) |
mark(0) |
mark(U11(x0,x1)) |
mark(tt) |
mark(s(x0)) |
mark(length(x0)) |
mark(and(x0,x1)) |
mark(isNat(x0)) |
mark(isNatList(x0)) |
mark(isNatIList(x0)) |
mark(nil) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
isNat#(active(X)) | → | isNat#(X) | (109) |
1 | > | 1 | |
isNat#(mark(X)) | → | isNat#(X) | (108) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
isNatList#(active(X)) | → | isNatList#(X) | (111) |
isNatList#(mark(X)) | → | isNatList#(X) | (110) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
We restrict the innermost strategy to the following left hand sides.
active(zeros) |
active(U11(tt,x0)) |
active(and(tt,x0)) |
active(isNat(0)) |
active(isNat(length(x0))) |
active(isNat(s(x0))) |
active(isNatIList(x0)) |
active(isNatList(nil)) |
active(isNatList(cons(x0,x1))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(zeros) |
mark(cons(x0,x1)) |
mark(0) |
mark(U11(x0,x1)) |
mark(tt) |
mark(s(x0)) |
mark(length(x0)) |
mark(and(x0,x1)) |
mark(isNat(x0)) |
mark(isNatList(x0)) |
mark(isNatIList(x0)) |
mark(nil) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
isNatList#(active(X)) | → | isNatList#(X) | (111) |
1 | > | 1 | |
isNatList#(mark(X)) | → | isNatList#(X) | (110) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
isNatIList#(active(X)) | → | isNatIList#(X) | (113) |
isNatIList#(mark(X)) | → | isNatIList#(X) | (112) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
We restrict the innermost strategy to the following left hand sides.
active(zeros) |
active(U11(tt,x0)) |
active(and(tt,x0)) |
active(isNat(0)) |
active(isNat(length(x0))) |
active(isNat(s(x0))) |
active(isNatIList(x0)) |
active(isNatList(nil)) |
active(isNatList(cons(x0,x1))) |
active(length(nil)) |
active(length(cons(x0,x1))) |
mark(zeros) |
mark(cons(x0,x1)) |
mark(0) |
mark(U11(x0,x1)) |
mark(tt) |
mark(s(x0)) |
mark(length(x0)) |
mark(and(x0,x1)) |
mark(isNat(x0)) |
mark(isNatList(x0)) |
mark(isNatIList(x0)) |
mark(nil) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
isNatIList#(active(X)) | → | isNatIList#(X) | (113) |
1 | > | 1 | |
isNatIList#(mark(X)) | → | isNatIList#(X) | (112) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.