The rewrite relation of the following TRS is considered.
active(U11(tt,V2)) | → | mark(U12(isNat(V2))) | (1) |
active(U12(tt)) | → | mark(tt) | (2) |
active(U21(tt)) | → | mark(tt) | (3) |
active(U31(tt,V2)) | → | mark(U32(isNat(V2))) | (4) |
active(U32(tt)) | → | mark(tt) | (5) |
active(U41(tt,N)) | → | mark(N) | (6) |
active(U51(tt,M,N)) | → | mark(U52(isNat(N),M,N)) | (7) |
active(U52(tt,M,N)) | → | mark(s(plus(N,M))) | (8) |
active(U61(tt)) | → | mark(0) | (9) |
active(U71(tt,M,N)) | → | mark(U72(isNat(N),M,N)) | (10) |
active(U72(tt,M,N)) | → | mark(plus(x(N,M),N)) | (11) |
active(isNat(0)) | → | mark(tt) | (12) |
active(isNat(plus(V1,V2))) | → | mark(U11(isNat(V1),V2)) | (13) |
active(isNat(s(V1))) | → | mark(U21(isNat(V1))) | (14) |
active(isNat(x(V1,V2))) | → | mark(U31(isNat(V1),V2)) | (15) |
active(plus(N,0)) | → | mark(U41(isNat(N),N)) | (16) |
active(plus(N,s(M))) | → | mark(U51(isNat(M),M,N)) | (17) |
active(x(N,0)) | → | mark(U61(isNat(N))) | (18) |
active(x(N,s(M))) | → | mark(U71(isNat(M),M,N)) | (19) |
mark(U11(X1,X2)) | → | active(U11(mark(X1),X2)) | (20) |
mark(tt) | → | active(tt) | (21) |
mark(U12(X)) | → | active(U12(mark(X))) | (22) |
mark(isNat(X)) | → | active(isNat(X)) | (23) |
mark(U21(X)) | → | active(U21(mark(X))) | (24) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (25) |
mark(U32(X)) | → | active(U32(mark(X))) | (26) |
mark(U41(X1,X2)) | → | active(U41(mark(X1),X2)) | (27) |
mark(U51(X1,X2,X3)) | → | active(U51(mark(X1),X2,X3)) | (28) |
mark(U52(X1,X2,X3)) | → | active(U52(mark(X1),X2,X3)) | (29) |
mark(s(X)) | → | active(s(mark(X))) | (30) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (31) |
mark(U61(X)) | → | active(U61(mark(X))) | (32) |
mark(0) | → | active(0) | (33) |
mark(U71(X1,X2,X3)) | → | active(U71(mark(X1),X2,X3)) | (34) |
mark(U72(X1,X2,X3)) | → | active(U72(mark(X1),X2,X3)) | (35) |
mark(x(X1,X2)) | → | active(x(mark(X1),mark(X2))) | (36) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
isNat(mark(X)) | → | isNat(X) | (43) |
isNat(active(X)) | → | isNat(X) | (44) |
U21(mark(X)) | → | U21(X) | (45) |
U21(active(X)) | → | U21(X) | (46) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U32(mark(X)) | → | U32(X) | (51) |
U32(active(X)) | → | U32(X) | (52) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
s(mark(X)) | → | s(X) | (69) |
s(active(X)) | → | s(X) | (70) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U61(active(X)) | → | U61(X) | (76) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
x(mark(X1),X2) | → | x(X1,X2) | (89) |
x(X1,mark(X2)) | → | x(X1,X2) | (90) |
x(active(X1),X2) | → | x(X1,X2) | (91) |
x(X1,active(X2)) | → | x(X1,X2) | (92) |
There are 148 ruless (increase limit for explicit display).
The dependency pairs are split into 16 components.
mark#(U41(X1,X2)) | → | mark#(X1) | (237) |
mark#(U52(X1,X2,X3)) | → | active#(U52(mark(X1),X2,X3)) | (236) |
active#(plus(N,s(M))) | → | mark#(U51(isNat(M),M,N)) | (167) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (234) |
mark#(U61(X)) | → | mark#(X) | (165) |
mark#(plus(X1,X2)) | → | mark#(X2) | (161) |
mark#(x(X1,X2)) | → | active#(x(mark(X1),mark(X2))) | (231) |
active#(U31(tt,V2)) | → | mark#(U32(isNat(V2))) | (230) |
mark#(U12(X)) | → | mark#(X) | (155) |
mark#(U21(X)) | → | mark#(X) | (154) |
mark#(x(X1,X2)) | → | mark#(X2) | (227) |
mark#(U32(X)) | → | mark#(X) | (152) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
active#(U51(tt,M,N)) | → | mark#(U52(isNat(N),M,N)) | (224) |
mark#(U31(X1,X2)) | → | active#(U31(mark(X1),X2)) | (148) |
mark#(U61(X)) | → | active#(U61(mark(X))) | (144) |
mark#(U12(X)) | → | active#(U12(mark(X))) | (145) |
active#(U11(tt,V2)) | → | mark#(U12(isNat(V2))) | (219) |
mark#(U72(X1,X2,X3)) | → | mark#(X1) | (139) |
active#(U52(tt,M,N)) | → | mark#(s(plus(N,M))) | (212) |
active#(x(N,0)) | → | mark#(U61(isNat(N))) | (135) |
mark#(s(X)) | → | mark#(X) | (132) |
mark#(plus(X1,X2)) | → | mark#(X1) | (131) |
mark#(U52(X1,X2,X3)) | → | mark#(X1) | (127) |
mark#(U32(X)) | → | active#(U32(mark(X))) | (126) |
active#(U41(tt,N)) | → | mark#(N) | (200) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
active#(U72(tt,M,N)) | → | mark#(plus(x(N,M),N)) | (125) |
active#(isNat(x(V1,V2))) | → | mark#(U31(isNat(V1),V2)) | (122) |
active#(x(N,s(M))) | → | mark#(U71(isNat(M),M,N)) | (119) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
mark#(x(X1,X2)) | → | mark#(X1) | (117) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (112) |
mark#(s(X)) | → | active#(s(mark(X))) | (192) |
mark#(U11(X1,X2)) | → | active#(U11(mark(X1),X2)) | (110) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U51(X1,X2,X3)) | → | active#(U51(mark(X1),X2,X3)) | (109) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
mark#(U71(X1,X2,X3)) | → | mark#(X1) | (107) |
mark#(U31(X1,X2)) | → | mark#(X1) | (188) |
mark#(U51(X1,X2,X3)) | → | mark#(X1) | (185) |
mark#(U72(X1,X2,X3)) | → | active#(U72(mark(X1),X2,X3)) | (179) |
active#(plus(N,0)) | → | mark#(U41(isNat(N),N)) | (177) |
mark#(U21(X)) | → | active#(U21(mark(X))) | (95) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 591 |
[U11(x1, x2)] | = | 48030 |
[s(x1)] | = | 841 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | 48030 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | 48030 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 18588 |
[x(x1, x2)] | = | 48030 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 48030 |
[0] | = | 1 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 1 |
[U32(x1)] | = | 1 |
[isNat(x1)] | = | 48030 |
[U52(x1, x2, x3)] | = | 48030 |
[plus(x1, x2)] | = | 48030 |
[U61(x1)] | = | 19148 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | 1 |
[U31(x1, x2)] | = | 48030 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | x1 + 0 |
[U21#(x1)] | = | 0 |
[tt] | = | 1 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | 48030 |
[U41(x1, x2)] | = | 48030 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
active(x(N,0)) | → | mark(U61(isNat(N))) | (18) |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
active(U31(tt,V2)) | → | mark(U32(isNat(V2))) | (4) |
active(isNat(x(V1,V2))) | → | mark(U31(isNat(V1),V2)) | (15) |
active(U52(tt,M,N)) | → | mark(s(plus(N,M))) | (8) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
active(U11(tt,V2)) | → | mark(U12(isNat(V2))) | (1) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
active(U21(tt)) | → | mark(tt) | (3) |
active(plus(N,0)) | → | mark(U41(isNat(N),N)) | (16) |
mark(tt) | → | active(tt) | (21) |
mark(x(X1,X2)) | → | active(x(mark(X1),mark(X2))) | (36) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
mark(U32(X)) | → | active(U32(mark(X))) | (26) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
active(x(N,s(M))) | → | mark(U71(isNat(M),M,N)) | (19) |
mark(U61(X)) | → | active(U61(mark(X))) | (32) |
active(plus(N,s(M))) | → | mark(U51(isNat(M),M,N)) | (17) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
mark(U41(X1,X2)) | → | active(U41(mark(X1),X2)) | (27) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
mark(U71(X1,X2,X3)) | → | active(U71(mark(X1),X2,X3)) | (34) |
mark(U12(X)) | → | active(U12(mark(X))) | (22) |
mark(U51(X1,X2,X3)) | → | active(U51(mark(X1),X2,X3)) | (28) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
active(U32(tt)) | → | mark(tt) | (5) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
mark(0) | → | active(0) | (33) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
x(X1,active(X2)) | → | x(X1,X2) | (92) |
active(U71(tt,M,N)) | → | mark(U72(isNat(N),M,N)) | (10) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
active(U51(tt,M,N)) | → | mark(U52(isNat(N),M,N)) | (7) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
mark(U11(X1,X2)) | → | active(U11(mark(X1),X2)) | (20) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (25) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
mark(s(X)) | → | active(s(mark(X))) | (30) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
active(isNat(s(V1))) | → | mark(U21(isNat(V1))) | (14) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
x(mark(X1),X2) | → | x(X1,X2) | (89) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (31) |
active(isNat(0)) | → | mark(tt) | (12) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
mark(isNat(X)) | → | active(isNat(X)) | (23) |
s(active(X)) | → | s(X) | (70) |
mark(U21(X)) | → | active(U21(mark(X))) | (24) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
active(U72(tt,M,N)) | → | mark(plus(x(N,M),N)) | (11) |
active(U61(tt)) | → | mark(0) | (9) |
active(isNat(plus(V1,V2))) | → | mark(U11(isNat(V1),V2)) | (13) |
U32(mark(X)) | → | U32(X) | (51) |
x(X1,mark(X2)) | → | x(X1,X2) | (90) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
active(U41(tt,N)) | → | mark(N) | (6) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
x(active(X1),X2) | → | x(X1,X2) | (91) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
mark(U72(X1,X2,X3)) | → | active(U72(mark(X1),X2,X3)) | (35) |
mark(U52(X1,X2,X3)) | → | active(U52(mark(X1),X2,X3)) | (29) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
active(U12(tt)) | → | mark(tt) | (2) |
mark#(U61(X)) | → | active#(U61(mark(X))) | (144) |
mark#(U12(X)) | → | active#(U12(mark(X))) | (145) |
mark#(U32(X)) | → | active#(U32(mark(X))) | (126) |
mark#(s(X)) | → | active#(s(mark(X))) | (192) |
mark#(U21(X)) | → | active#(U21(mark(X))) | (95) |
The dependency pairs are split into 1 component.
active#(x(N,0)) | → | mark#(U61(isNat(N))) | (135) |
active#(U31(tt,V2)) | → | mark#(U32(isNat(V2))) | (230) |
active#(isNat(x(V1,V2))) | → | mark#(U31(isNat(V1),V2)) | (122) |
active#(U52(tt,M,N)) | → | mark#(s(plus(N,M))) | (212) |
active#(U11(tt,V2)) | → | mark#(U12(isNat(V2))) | (219) |
active#(plus(N,0)) | → | mark#(U41(isNat(N),N)) | (177) |
mark#(x(X1,X2)) | → | mark#(X2) | (227) |
mark#(x(X1,X2)) | → | mark#(X1) | (117) |
mark#(x(X1,X2)) | → | active#(x(mark(X1),mark(X2))) | (231) |
mark#(U32(X)) | → | mark#(X) | (152) |
active#(x(N,s(M))) | → | mark#(U71(isNat(M),M,N)) | (119) |
mark#(U61(X)) | → | mark#(X) | (165) |
active#(plus(N,s(M))) | → | mark#(U51(isNat(M),M,N)) | (167) |
mark#(U41(X1,X2)) | → | mark#(X1) | (237) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (234) |
mark#(U71(X1,X2,X3)) | → | mark#(X1) | (107) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
mark#(U12(X)) | → | mark#(X) | (155) |
mark#(U51(X1,X2,X3)) | → | mark#(X1) | (185) |
mark#(U51(X1,X2,X3)) | → | active#(U51(mark(X1),X2,X3)) | (109) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
active#(U51(tt,M,N)) | → | mark#(U52(isNat(N),M,N)) | (224) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
mark#(U11(X1,X2)) | → | active#(U11(mark(X1),X2)) | (110) |
mark#(U31(X1,X2)) | → | mark#(X1) | (188) |
mark#(U31(X1,X2)) | → | active#(U31(mark(X1),X2)) | (148) |
mark#(s(X)) | → | mark#(X) | (132) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(plus(X1,X2)) | → | mark#(X2) | (161) |
mark#(plus(X1,X2)) | → | mark#(X1) | (131) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (112) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(U72(tt,M,N)) | → | mark#(plus(x(N,M),N)) | (125) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
active#(U41(tt,N)) | → | mark#(N) | (200) |
mark#(U72(X1,X2,X3)) | → | mark#(X1) | (139) |
mark#(U72(X1,X2,X3)) | → | active#(U72(mark(X1),X2,X3)) | (179) |
mark#(U52(X1,X2,X3)) | → | mark#(X1) | (127) |
mark#(U52(X1,X2,X3)) | → | active#(U52(mark(X1),X2,X3)) | (236) |
[U72#(x1, x2, x3)] | = | max(0) |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 0 |
[U11(x1, x2)] | = | max(x1 + 0, 0) |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | max(x1 + 1, x2 + 842, x3 + 17752, 0) |
[plus#(x1, x2)] | = | max(0) |
[U72(x1, x2, x3)] | = | max(x1 + 1, x2 + 842, x3 + 17752, 0) |
[U52#(x1, x2, x3)] | = | max(0) |
[U12(x1)] | = | x1 + 0 |
[x(x1, x2)] | = | max(x1 + 17752, x2 + 842, 0) |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 4330 |
[x#(x1, x2)] | = | max(0) |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[U32(x1)] | = | x1 + 0 |
[isNat(x1)] | = | 842 |
[U52(x1, x2, x3)] | = | max(x1 + 16909, x2 + 17751, x3 + 0, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 17751, 0) |
[U61(x1)] | = | x1 + 4329 |
[U51#(x1, x2, x3)] | = | max(0) |
[U11#(x1, x2)] | = | max(0) |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | max(x1 + 0, 0) |
[U41#(x1, x2)] | = | max(0) |
[active#(x1)] | = | x1 + 0 |
[U21#(x1)] | = | 0 |
[tt] | = | 842 |
[U71#(x1, x2, x3)] | = | max(0) |
[U51(x1, x2, x3)] | = | max(x1 + 16909, x2 + 17751, x3 + 0, 0) |
[U41(x1, x2)] | = | max(x1 + 2374, x2 + 0, 0) |
[U31#(x1, x2)] | = | max(0) |
[U61#(x1)] | = | 0 |
active(x(N,0)) | → | mark(U61(isNat(N))) | (18) |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
active(U31(tt,V2)) | → | mark(U32(isNat(V2))) | (4) |
active(isNat(x(V1,V2))) | → | mark(U31(isNat(V1),V2)) | (15) |
active(U52(tt,M,N)) | → | mark(s(plus(N,M))) | (8) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
active(U11(tt,V2)) | → | mark(U12(isNat(V2))) | (1) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
active(U21(tt)) | → | mark(tt) | (3) |
active(plus(N,0)) | → | mark(U41(isNat(N),N)) | (16) |
mark(tt) | → | active(tt) | (21) |
mark(x(X1,X2)) | → | active(x(mark(X1),mark(X2))) | (36) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
mark(U32(X)) | → | active(U32(mark(X))) | (26) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
active(x(N,s(M))) | → | mark(U71(isNat(M),M,N)) | (19) |
mark(U61(X)) | → | active(U61(mark(X))) | (32) |
active(plus(N,s(M))) | → | mark(U51(isNat(M),M,N)) | (17) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
mark(U41(X1,X2)) | → | active(U41(mark(X1),X2)) | (27) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
mark(U71(X1,X2,X3)) | → | active(U71(mark(X1),X2,X3)) | (34) |
mark(U12(X)) | → | active(U12(mark(X))) | (22) |
mark(U51(X1,X2,X3)) | → | active(U51(mark(X1),X2,X3)) | (28) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
active(U32(tt)) | → | mark(tt) | (5) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
mark(0) | → | active(0) | (33) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
x(X1,active(X2)) | → | x(X1,X2) | (92) |
active(U71(tt,M,N)) | → | mark(U72(isNat(N),M,N)) | (10) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
active(U51(tt,M,N)) | → | mark(U52(isNat(N),M,N)) | (7) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
mark(U11(X1,X2)) | → | active(U11(mark(X1),X2)) | (20) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (25) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
mark(s(X)) | → | active(s(mark(X))) | (30) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
active(isNat(s(V1))) | → | mark(U21(isNat(V1))) | (14) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
x(mark(X1),X2) | → | x(X1,X2) | (89) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (31) |
active(isNat(0)) | → | mark(tt) | (12) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
mark(isNat(X)) | → | active(isNat(X)) | (23) |
s(active(X)) | → | s(X) | (70) |
mark(U21(X)) | → | active(U21(mark(X))) | (24) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
active(U72(tt,M,N)) | → | mark(plus(x(N,M),N)) | (11) |
active(U61(tt)) | → | mark(0) | (9) |
active(isNat(plus(V1,V2))) | → | mark(U11(isNat(V1),V2)) | (13) |
U32(mark(X)) | → | U32(X) | (51) |
x(X1,mark(X2)) | → | x(X1,X2) | (90) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
active(U41(tt,N)) | → | mark(N) | (6) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
x(active(X1),X2) | → | x(X1,X2) | (91) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
mark(U72(X1,X2,X3)) | → | active(U72(mark(X1),X2,X3)) | (35) |
mark(U52(X1,X2,X3)) | → | active(U52(mark(X1),X2,X3)) | (29) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
active(U12(tt)) | → | mark(tt) | (2) |
active#(x(N,0)) | → | mark#(U61(isNat(N))) | (135) |
mark#(x(X1,X2)) | → | mark#(X2) | (227) |
mark#(x(X1,X2)) | → | mark#(X1) | (117) |
mark#(U61(X)) | → | mark#(X) | (165) |
mark#(U41(X1,X2)) | → | mark#(X1) | (237) |
mark#(U71(X1,X2,X3)) | → | mark#(X1) | (107) |
mark#(U51(X1,X2,X3)) | → | mark#(X1) | (185) |
mark#(plus(X1,X2)) | → | mark#(X2) | (161) |
mark#(U72(X1,X2,X3)) | → | mark#(X1) | (139) |
mark#(U52(X1,X2,X3)) | → | mark#(X1) | (127) |
The dependency pairs are split into 1 component.
active#(U31(tt,V2)) | → | mark#(U32(isNat(V2))) | (230) |
active#(isNat(x(V1,V2))) | → | mark#(U31(isNat(V1),V2)) | (122) |
active#(U52(tt,M,N)) | → | mark#(s(plus(N,M))) | (212) |
active#(U11(tt,V2)) | → | mark#(U12(isNat(V2))) | (219) |
active#(plus(N,0)) | → | mark#(U41(isNat(N),N)) | (177) |
mark#(x(X1,X2)) | → | active#(x(mark(X1),mark(X2))) | (231) |
mark#(U32(X)) | → | mark#(X) | (152) |
active#(x(N,s(M))) | → | mark#(U71(isNat(M),M,N)) | (119) |
active#(plus(N,s(M))) | → | mark#(U51(isNat(M),M,N)) | (167) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (234) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
mark#(U12(X)) | → | mark#(X) | (155) |
mark#(U51(X1,X2,X3)) | → | active#(U51(mark(X1),X2,X3)) | (109) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
active#(U51(tt,M,N)) | → | mark#(U52(isNat(N),M,N)) | (224) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
mark#(U11(X1,X2)) | → | active#(U11(mark(X1),X2)) | (110) |
mark#(U31(X1,X2)) | → | mark#(X1) | (188) |
mark#(U31(X1,X2)) | → | active#(U31(mark(X1),X2)) | (148) |
mark#(s(X)) | → | mark#(X) | (132) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(plus(X1,X2)) | → | mark#(X1) | (131) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (112) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(U72(tt,M,N)) | → | mark#(plus(x(N,M),N)) | (125) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
active#(U41(tt,N)) | → | mark#(N) | (200) |
mark#(U72(X1,X2,X3)) | → | active#(U72(mark(X1),X2,X3)) | (179) |
mark#(U52(X1,X2,X3)) | → | active#(U52(mark(X1),X2,X3)) | (236) |
[U72#(x1, x2, x3)] | = | max(0) |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 0 |
[U11(x1, x2)] | = | max(x1 + 0, x2 + 63491, 0) |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | max(x2 + 3, x3 + 31747, 0) |
[plus#(x1, x2)] | = | max(0) |
[U72(x1, x2, x3)] | = | max(x1 + 0, x2 + 3, x3 + 31747, 0) |
[U52#(x1, x2, x3)] | = | max(0) |
[U12(x1)] | = | x1 + 28940 |
[x(x1, x2)] | = | max(x1 + 31747, x2 + 3, 0) |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 31744 |
[x#(x1, x2)] | = | max(0) |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[U32(x1)] | = | x1 + 0 |
[isNat(x1)] | = | x1 + 31746 |
[U52(x1, x2, x3)] | = | max(x2 + 31746, x3 + 0, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 31746, 0) |
[U61(x1)] | = | x1 + 1 |
[U51#(x1, x2, x3)] | = | max(0) |
[U11#(x1, x2)] | = | max(0) |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | max(x1 + 1, x2 + 31747, 0) |
[U41#(x1, x2)] | = | max(0) |
[active#(x1)] | = | x1 + 0 |
[U21#(x1)] | = | 0 |
[tt] | = | 60685 |
[U71#(x1, x2, x3)] | = | max(0) |
[U51(x1, x2, x3)] | = | max(x2 + 31746, x3 + 0, 0) |
[U41(x1, x2)] | = | max(x2 + 0, 0) |
[U31#(x1, x2)] | = | max(0) |
[U61#(x1)] | = | 0 |
active(x(N,0)) | → | mark(U61(isNat(N))) | (18) |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
active(U31(tt,V2)) | → | mark(U32(isNat(V2))) | (4) |
active(isNat(x(V1,V2))) | → | mark(U31(isNat(V1),V2)) | (15) |
active(U52(tt,M,N)) | → | mark(s(plus(N,M))) | (8) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
active(U11(tt,V2)) | → | mark(U12(isNat(V2))) | (1) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
active(U21(tt)) | → | mark(tt) | (3) |
active(plus(N,0)) | → | mark(U41(isNat(N),N)) | (16) |
mark(tt) | → | active(tt) | (21) |
mark(x(X1,X2)) | → | active(x(mark(X1),mark(X2))) | (36) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
mark(U32(X)) | → | active(U32(mark(X))) | (26) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
active(x(N,s(M))) | → | mark(U71(isNat(M),M,N)) | (19) |
mark(U61(X)) | → | active(U61(mark(X))) | (32) |
active(plus(N,s(M))) | → | mark(U51(isNat(M),M,N)) | (17) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
mark(U41(X1,X2)) | → | active(U41(mark(X1),X2)) | (27) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
mark(U71(X1,X2,X3)) | → | active(U71(mark(X1),X2,X3)) | (34) |
mark(U12(X)) | → | active(U12(mark(X))) | (22) |
mark(U51(X1,X2,X3)) | → | active(U51(mark(X1),X2,X3)) | (28) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
active(U32(tt)) | → | mark(tt) | (5) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
mark(0) | → | active(0) | (33) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
x(X1,active(X2)) | → | x(X1,X2) | (92) |
active(U71(tt,M,N)) | → | mark(U72(isNat(N),M,N)) | (10) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
active(U51(tt,M,N)) | → | mark(U52(isNat(N),M,N)) | (7) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
mark(U11(X1,X2)) | → | active(U11(mark(X1),X2)) | (20) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (25) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
mark(s(X)) | → | active(s(mark(X))) | (30) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
active(isNat(s(V1))) | → | mark(U21(isNat(V1))) | (14) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
x(mark(X1),X2) | → | x(X1,X2) | (89) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (31) |
active(isNat(0)) | → | mark(tt) | (12) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
mark(isNat(X)) | → | active(isNat(X)) | (23) |
s(active(X)) | → | s(X) | (70) |
mark(U21(X)) | → | active(U21(mark(X))) | (24) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
active(U72(tt,M,N)) | → | mark(plus(x(N,M),N)) | (11) |
active(U61(tt)) | → | mark(0) | (9) |
active(isNat(plus(V1,V2))) | → | mark(U11(isNat(V1),V2)) | (13) |
U32(mark(X)) | → | U32(X) | (51) |
x(X1,mark(X2)) | → | x(X1,X2) | (90) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
active(U41(tt,N)) | → | mark(N) | (6) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
x(active(X1),X2) | → | x(X1,X2) | (91) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
mark(U72(X1,X2,X3)) | → | active(U72(mark(X1),X2,X3)) | (35) |
mark(U52(X1,X2,X3)) | → | active(U52(mark(X1),X2,X3)) | (29) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
active(U12(tt)) | → | mark(tt) | (2) |
active#(U31(tt,V2)) | → | mark#(U32(isNat(V2))) | (230) |
active#(isNat(x(V1,V2))) | → | mark#(U31(isNat(V1),V2)) | (122) |
active#(U11(tt,V2)) | → | mark#(U12(isNat(V2))) | (219) |
mark#(U12(X)) | → | mark#(X) | (155) |
mark#(U31(X1,X2)) | → | mark#(X1) | (188) |
The dependency pairs are split into 1 component.
active#(U52(tt,M,N)) | → | mark#(s(plus(N,M))) | (212) |
active#(plus(N,0)) | → | mark#(U41(isNat(N),N)) | (177) |
mark#(x(X1,X2)) | → | active#(x(mark(X1),mark(X2))) | (231) |
mark#(U32(X)) | → | mark#(X) | (152) |
active#(x(N,s(M))) | → | mark#(U71(isNat(M),M,N)) | (119) |
active#(plus(N,s(M))) | → | mark#(U51(isNat(M),M,N)) | (167) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (234) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
mark#(U51(X1,X2,X3)) | → | active#(U51(mark(X1),X2,X3)) | (109) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
active#(U51(tt,M,N)) | → | mark#(U52(isNat(N),M,N)) | (224) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
mark#(U11(X1,X2)) | → | active#(U11(mark(X1),X2)) | (110) |
mark#(U31(X1,X2)) | → | active#(U31(mark(X1),X2)) | (148) |
mark#(s(X)) | → | mark#(X) | (132) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(plus(X1,X2)) | → | mark#(X1) | (131) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (112) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(U72(tt,M,N)) | → | mark#(plus(x(N,M),N)) | (125) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
active#(U41(tt,N)) | → | mark#(N) | (200) |
mark#(U72(X1,X2,X3)) | → | active#(U72(mark(X1),X2,X3)) | (179) |
mark#(U52(X1,X2,X3)) | → | active#(U52(mark(X1),X2,X3)) | (236) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 1 |
[U11(x1, x2)] | = | 1 |
[s(x1)] | = | 0 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | 17019 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | 17019 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 25 |
[x(x1, x2)] | = | 17019 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 65049 |
[0] | = | 24 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 1 |
[U32(x1)] | = | 1 |
[isNat(x1)] | = | 17019 |
[U52(x1, x2, x3)] | = | 17019 |
[plus(x1, x2)] | = | 17019 |
[U61(x1)] | = | 25 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | 2 |
[U31(x1, x2)] | = | 3 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | x1 + 48030 |
[U21#(x1)] | = | 0 |
[tt] | = | 1 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | 17019 |
[U41(x1, x2)] | = | 17019 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
x(X1,active(X2)) | → | x(X1,X2) | (92) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
x(mark(X1),X2) | → | x(X1,X2) | (89) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
s(active(X)) | → | s(X) | (70) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
U32(mark(X)) | → | U32(X) | (51) |
x(X1,mark(X2)) | → | x(X1,X2) | (90) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
x(active(X1),X2) | → | x(X1,X2) | (91) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
mark#(U11(X1,X2)) | → | active#(U11(mark(X1),X2)) | (110) |
mark#(U31(X1,X2)) | → | active#(U31(mark(X1),X2)) | (148) |
The dependency pairs are split into 1 component.
active#(U52(tt,M,N)) | → | mark#(s(plus(N,M))) | (212) |
active#(plus(N,0)) | → | mark#(U41(isNat(N),N)) | (177) |
mark#(x(X1,X2)) | → | active#(x(mark(X1),mark(X2))) | (231) |
mark#(U32(X)) | → | mark#(X) | (152) |
active#(x(N,s(M))) | → | mark#(U71(isNat(M),M,N)) | (119) |
active#(plus(N,s(M))) | → | mark#(U51(isNat(M),M,N)) | (167) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (234) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
mark#(U51(X1,X2,X3)) | → | active#(U51(mark(X1),X2,X3)) | (109) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
active#(U51(tt,M,N)) | → | mark#(U52(isNat(N),M,N)) | (224) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
mark#(s(X)) | → | mark#(X) | (132) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(plus(X1,X2)) | → | mark#(X1) | (131) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (112) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(U72(tt,M,N)) | → | mark#(plus(x(N,M),N)) | (125) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
active#(U41(tt,N)) | → | mark#(N) | (200) |
mark#(U72(X1,X2,X3)) | → | active#(U72(mark(X1),X2,X3)) | (179) |
mark#(U52(X1,X2,X3)) | → | active#(U52(mark(X1),X2,X3)) | (236) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 0 |
[U11(x1, x2)] | = | x1 + 0 |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x2 + x3 + 1 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x2 + x3 + 1 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 1 |
[x(x1, x2)] | = | x1 + x2 + 1 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 48030 |
[0] | = | 0 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[U32(x1)] | = | x1 + 1 |
[isNat(x1)] | = | x1 + 1 |
[U52(x1, x2, x3)] | = | x3 + 0 |
[plus(x1, x2)] | = | x1 + 0 |
[U61(x1)] | = | 1 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | x1 + x2 + 1 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | x1 + 48030 |
[U21#(x1)] | = | 0 |
[tt] | = | 1 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x3 + 0 |
[U41(x1, x2)] | = | x2 + 0 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
active(x(N,0)) | → | mark(U61(isNat(N))) | (18) |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
active(U31(tt,V2)) | → | mark(U32(isNat(V2))) | (4) |
active(isNat(x(V1,V2))) | → | mark(U31(isNat(V1),V2)) | (15) |
active(U52(tt,M,N)) | → | mark(s(plus(N,M))) | (8) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
active(U11(tt,V2)) | → | mark(U12(isNat(V2))) | (1) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
active(U21(tt)) | → | mark(tt) | (3) |
active(plus(N,0)) | → | mark(U41(isNat(N),N)) | (16) |
mark(tt) | → | active(tt) | (21) |
mark(x(X1,X2)) | → | active(x(mark(X1),mark(X2))) | (36) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
mark(U32(X)) | → | active(U32(mark(X))) | (26) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
active(x(N,s(M))) | → | mark(U71(isNat(M),M,N)) | (19) |
mark(U61(X)) | → | active(U61(mark(X))) | (32) |
active(plus(N,s(M))) | → | mark(U51(isNat(M),M,N)) | (17) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
mark(U41(X1,X2)) | → | active(U41(mark(X1),X2)) | (27) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
mark(U71(X1,X2,X3)) | → | active(U71(mark(X1),X2,X3)) | (34) |
mark(U12(X)) | → | active(U12(mark(X))) | (22) |
mark(U51(X1,X2,X3)) | → | active(U51(mark(X1),X2,X3)) | (28) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
active(U32(tt)) | → | mark(tt) | (5) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
mark(0) | → | active(0) | (33) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
x(X1,active(X2)) | → | x(X1,X2) | (92) |
active(U71(tt,M,N)) | → | mark(U72(isNat(N),M,N)) | (10) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
active(U51(tt,M,N)) | → | mark(U52(isNat(N),M,N)) | (7) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
mark(U11(X1,X2)) | → | active(U11(mark(X1),X2)) | (20) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (25) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
mark(s(X)) | → | active(s(mark(X))) | (30) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
active(isNat(s(V1))) | → | mark(U21(isNat(V1))) | (14) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
x(mark(X1),X2) | → | x(X1,X2) | (89) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (31) |
active(isNat(0)) | → | mark(tt) | (12) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
mark(isNat(X)) | → | active(isNat(X)) | (23) |
s(active(X)) | → | s(X) | (70) |
mark(U21(X)) | → | active(U21(mark(X))) | (24) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
active(U72(tt,M,N)) | → | mark(plus(x(N,M),N)) | (11) |
active(U61(tt)) | → | mark(0) | (9) |
active(isNat(plus(V1,V2))) | → | mark(U11(isNat(V1),V2)) | (13) |
U32(mark(X)) | → | U32(X) | (51) |
x(X1,mark(X2)) | → | x(X1,X2) | (90) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
active(U41(tt,N)) | → | mark(N) | (6) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
x(active(X1),X2) | → | x(X1,X2) | (91) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
mark(U72(X1,X2,X3)) | → | active(U72(mark(X1),X2,X3)) | (35) |
mark(U52(X1,X2,X3)) | → | active(U52(mark(X1),X2,X3)) | (29) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
active(U12(tt)) | → | mark(tt) | (2) |
mark#(U32(X)) | → | mark#(X) | (152) |
The dependency pairs are split into 1 component.
active#(U52(tt,M,N)) | → | mark#(s(plus(N,M))) | (212) |
active#(plus(N,0)) | → | mark#(U41(isNat(N),N)) | (177) |
mark#(x(X1,X2)) | → | active#(x(mark(X1),mark(X2))) | (231) |
active#(x(N,s(M))) | → | mark#(U71(isNat(M),M,N)) | (119) |
active#(plus(N,s(M))) | → | mark#(U51(isNat(M),M,N)) | (167) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (234) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
mark#(U51(X1,X2,X3)) | → | active#(U51(mark(X1),X2,X3)) | (109) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
active#(U51(tt,M,N)) | → | mark#(U52(isNat(N),M,N)) | (224) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
mark#(s(X)) | → | mark#(X) | (132) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(plus(X1,X2)) | → | mark#(X1) | (131) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (112) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(U72(tt,M,N)) | → | mark#(plus(x(N,M),N)) | (125) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
active#(U41(tt,N)) | → | mark#(N) | (200) |
mark#(U72(X1,X2,X3)) | → | active#(U72(mark(X1),X2,X3)) | (179) |
mark#(U52(X1,X2,X3)) | → | active#(U52(mark(X1),X2,X3)) | (236) |
π(U72#) | = | 1 |
π(U21) | = | 1 |
π(U11) | = | 1 |
π(plus#) | = | 1 |
π(U12) | = | 1 |
π(x#) | = | 1 |
π(s#) | = | 1 |
π(mark) | = | 1 |
π(U11#) | = | 2 |
π(active) | = | 1 |
π(U31) | = | 1 |
π(U21#) | = | 1 |
π(U71#) | = | 1 |
π(U41) | = | 2 |
prec(U32#) | = | 0 | status(U32#) | = | [] | list-extension(U32#) | = | Lex | ||
prec(s) | = | 2 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(isNat#) | = | 0 | status(isNat#) | = | [] | list-extension(isNat#) | = | Lex | ||
prec(U71) | = | 4 | status(U71) | = | [2, 3, 1] | list-extension(U71) | = | Lex | ||
prec(U72) | = | 4 | status(U72) | = | [2, 3, 1] | list-extension(U72) | = | Lex | ||
prec(U52#) | = | 0 | status(U52#) | = | [3, 2] | list-extension(U52#) | = | Lex | ||
prec(x) | = | 4 | status(x) | = | [2, 1] | list-extension(x) | = | Lex | ||
prec(U12#) | = | 0 | status(U12#) | = | [] | list-extension(U12#) | = | Lex | ||
prec(mark#) | = | 3 | status(mark#) | = | [1] | list-extension(mark#) | = | Lex | ||
prec(0) | = | 1 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(U32) | = | 1 | status(U32) | = | [] | list-extension(U32) | = | Lex | ||
prec(isNat) | = | 1 | status(isNat) | = | [] | list-extension(isNat) | = | Lex | ||
prec(U52) | = | 3 | status(U52) | = | [3, 2, 1] | list-extension(U52) | = | Lex | ||
prec(plus) | = | 3 | status(plus) | = | [1, 2] | list-extension(plus) | = | Lex | ||
prec(U61) | = | 4 | status(U61) | = | [1] | list-extension(U61) | = | Lex | ||
prec(U51#) | = | 0 | status(U51#) | = | [3, 2, 1] | list-extension(U51#) | = | Lex | ||
prec(U41#) | = | 0 | status(U41#) | = | [1, 2] | list-extension(U41#) | = | Lex | ||
prec(active#) | = | 3 | status(active#) | = | [1] | list-extension(active#) | = | Lex | ||
prec(tt) | = | 1 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(U51) | = | 3 | status(U51) | = | [3, 2, 1] | list-extension(U51) | = | Lex | ||
prec(U31#) | = | 0 | status(U31#) | = | [2, 1] | list-extension(U31#) | = | Lex | ||
prec(U61#) | = | 0 | status(U61#) | = | [] | list-extension(U61#) | = | Lex |
[U32#(x1)] | = | 0 |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U72(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U52#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 0 |
[U32(x1)] | = | 0 |
[isNat(x1)] | = | 0 |
[U52(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U61(x1)] | = | x1 + 0 |
[U51#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U41#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[active#(x1)] | = | x1 + 0 |
[tt] | = | 0 |
[U51(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U31#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U61#(x1)] | = | 0 |
active(x(N,0)) | → | mark(U61(isNat(N))) | (18) |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
active(U31(tt,V2)) | → | mark(U32(isNat(V2))) | (4) |
active(isNat(x(V1,V2))) | → | mark(U31(isNat(V1),V2)) | (15) |
active(U52(tt,M,N)) | → | mark(s(plus(N,M))) | (8) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
active(U11(tt,V2)) | → | mark(U12(isNat(V2))) | (1) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
active(U21(tt)) | → | mark(tt) | (3) |
active(plus(N,0)) | → | mark(U41(isNat(N),N)) | (16) |
mark(tt) | → | active(tt) | (21) |
mark(x(X1,X2)) | → | active(x(mark(X1),mark(X2))) | (36) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
mark(U32(X)) | → | active(U32(mark(X))) | (26) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
active(x(N,s(M))) | → | mark(U71(isNat(M),M,N)) | (19) |
mark(U61(X)) | → | active(U61(mark(X))) | (32) |
active(plus(N,s(M))) | → | mark(U51(isNat(M),M,N)) | (17) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
mark(U41(X1,X2)) | → | active(U41(mark(X1),X2)) | (27) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
mark(U71(X1,X2,X3)) | → | active(U71(mark(X1),X2,X3)) | (34) |
mark(U12(X)) | → | active(U12(mark(X))) | (22) |
mark(U51(X1,X2,X3)) | → | active(U51(mark(X1),X2,X3)) | (28) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
active(U32(tt)) | → | mark(tt) | (5) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
mark(0) | → | active(0) | (33) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
x(X1,active(X2)) | → | x(X1,X2) | (92) |
active(U71(tt,M,N)) | → | mark(U72(isNat(N),M,N)) | (10) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
active(U51(tt,M,N)) | → | mark(U52(isNat(N),M,N)) | (7) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
mark(U11(X1,X2)) | → | active(U11(mark(X1),X2)) | (20) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (25) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
mark(s(X)) | → | active(s(mark(X))) | (30) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
active(isNat(s(V1))) | → | mark(U21(isNat(V1))) | (14) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
x(mark(X1),X2) | → | x(X1,X2) | (89) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (31) |
active(isNat(0)) | → | mark(tt) | (12) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
mark(isNat(X)) | → | active(isNat(X)) | (23) |
s(active(X)) | → | s(X) | (70) |
mark(U21(X)) | → | active(U21(mark(X))) | (24) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
active(U72(tt,M,N)) | → | mark(plus(x(N,M),N)) | (11) |
active(U61(tt)) | → | mark(0) | (9) |
active(isNat(plus(V1,V2))) | → | mark(U11(isNat(V1),V2)) | (13) |
U32(mark(X)) | → | U32(X) | (51) |
x(X1,mark(X2)) | → | x(X1,X2) | (90) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
active(U41(tt,N)) | → | mark(N) | (6) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
x(active(X1),X2) | → | x(X1,X2) | (91) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
mark(U72(X1,X2,X3)) | → | active(U72(mark(X1),X2,X3)) | (35) |
mark(U52(X1,X2,X3)) | → | active(U52(mark(X1),X2,X3)) | (29) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
active(U12(tt)) | → | mark(tt) | (2) |
active#(U52(tt,M,N)) | → | mark#(s(plus(N,M))) | (212) |
active#(plus(N,0)) | → | mark#(U41(isNat(N),N)) | (177) |
active#(x(N,s(M))) | → | mark#(U71(isNat(M),M,N)) | (119) |
active#(plus(N,s(M))) | → | mark#(U51(isNat(M),M,N)) | (167) |
mark#(s(X)) | → | mark#(X) | (132) |
mark#(plus(X1,X2)) | → | mark#(X1) | (131) |
active#(U72(tt,M,N)) | → | mark#(plus(x(N,M),N)) | (125) |
The dependency pairs are split into 1 component.
mark#(x(X1,X2)) | → | active#(x(mark(X1),mark(X2))) | (231) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (234) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
mark#(U51(X1,X2,X3)) | → | active#(U51(mark(X1),X2,X3)) | (109) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
active#(U51(tt,M,N)) | → | mark#(U52(isNat(N),M,N)) | (224) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (112) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
active#(U41(tt,N)) | → | mark#(N) | (200) |
mark#(U72(X1,X2,X3)) | → | active#(U72(mark(X1),X2,X3)) | (179) |
mark#(U52(X1,X2,X3)) | → | active#(U52(mark(X1),X2,X3)) | (236) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 13862 |
[U11(x1, x2)] | = | 23889 |
[s(x1)] | = | 23889 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | 1 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | 1 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 23889 |
[x(x1, x2)] | = | 1 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 48031 |
[0] | = | 23889 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 23888 |
[U32(x1)] | = | 1920 |
[isNat(x1)] | = | 1 |
[U52(x1, x2, x3)] | = | 1 |
[plus(x1, x2)] | = | 0 |
[U61(x1)] | = | 6946 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | 6047 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | x1 + 48030 |
[U21#(x1)] | = | 0 |
[tt] | = | 23889 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | 1 |
[U41(x1, x2)] | = | 1 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
x(X1,active(X2)) | → | x(X1,X2) | (92) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
x(mark(X1),X2) | → | x(X1,X2) | (89) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
s(active(X)) | → | s(X) | (70) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
U32(mark(X)) | → | U32(X) | (51) |
x(X1,mark(X2)) | → | x(X1,X2) | (90) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
x(active(X1),X2) | → | x(X1,X2) | (91) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
mark#(plus(X1,X2)) | → | active#(plus(mark(X1),mark(X2))) | (112) |
The dependency pairs are split into 1 component.
mark#(x(X1,X2)) | → | active#(x(mark(X1),mark(X2))) | (231) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (234) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
mark#(U51(X1,X2,X3)) | → | active#(U51(mark(X1),X2,X3)) | (109) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
active#(U51(tt,M,N)) | → | mark#(U52(isNat(N),M,N)) | (224) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
active#(U41(tt,N)) | → | mark#(N) | (200) |
mark#(U72(X1,X2,X3)) | → | active#(U72(mark(X1),X2,X3)) | (179) |
mark#(U52(X1,X2,X3)) | → | active#(U52(mark(X1),X2,X3)) | (236) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 1 |
[U11(x1, x2)] | = | 26837 |
[s(x1)] | = | 31329 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | 2 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | 1 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 8509 |
[x(x1, x2)] | = | 1 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 48032 |
[0] | = | 4 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 3 |
[U32(x1)] | = | 1 |
[isNat(x1)] | = | 2 |
[U52(x1, x2, x3)] | = | 1 |
[plus(x1, x2)] | = | 0 |
[U61(x1)] | = | 1 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | 2 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | x1 + 48030 |
[U21#(x1)] | = | 0 |
[tt] | = | 23889 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | 2 |
[U41(x1, x2)] | = | 2 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
x(X1,active(X2)) | → | x(X1,X2) | (92) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
x(mark(X1),X2) | → | x(X1,X2) | (89) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
s(active(X)) | → | s(X) | (70) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
U32(mark(X)) | → | U32(X) | (51) |
x(X1,mark(X2)) | → | x(X1,X2) | (90) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
x(active(X1),X2) | → | x(X1,X2) | (91) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
mark#(x(X1,X2)) | → | active#(x(mark(X1),mark(X2))) | (231) |
mark#(U72(X1,X2,X3)) | → | active#(U72(mark(X1),X2,X3)) | (179) |
mark#(U52(X1,X2,X3)) | → | active#(U52(mark(X1),X2,X3)) | (236) |
The dependency pairs are split into 1 component.
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (234) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
mark#(U51(X1,X2,X3)) | → | active#(U51(mark(X1),X2,X3)) | (109) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
active#(U51(tt,M,N)) | → | mark#(U52(isNat(N),M,N)) | (224) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
active#(U41(tt,N)) | → | mark#(N) | (200) |
[U72#(x1, x2, x3)] | = | max(0) |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 0 |
[U11(x1, x2)] | = | max(x1 + 0, 0) |
[s(x1)] | = | 0 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | max(x3 + 3, 0) |
[plus#(x1, x2)] | = | max(0) |
[U72(x1, x2, x3)] | = | max(x1 + 1, x3 + 3, 0) |
[U52#(x1, x2, x3)] | = | max(0) |
[U12(x1)] | = | 0 |
[x(x1, x2)] | = | max(x1 + 3, 0) |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[0] | = | 1 |
[x#(x1, x2)] | = | max(0) |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[U32(x1)] | = | 0 |
[isNat(x1)] | = | 1 |
[U52(x1, x2, x3)] | = | max(0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 3, 0) |
[U61(x1)] | = | 3 |
[U51#(x1, x2, x3)] | = | max(0) |
[U11#(x1, x2)] | = | max(0) |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | max(0) |
[U41#(x1, x2)] | = | max(0) |
[active#(x1)] | = | x1 + 0 |
[U21#(x1)] | = | 0 |
[tt] | = | 0 |
[U71#(x1, x2, x3)] | = | max(0) |
[U51(x1, x2, x3)] | = | max(x1 + 1, 0) |
[U41(x1, x2)] | = | max(x1 + 1, x2 + 0, 0) |
[U31#(x1, x2)] | = | max(0) |
[U61#(x1)] | = | 0 |
active(x(N,0)) | → | mark(U61(isNat(N))) | (18) |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
active(U31(tt,V2)) | → | mark(U32(isNat(V2))) | (4) |
active(isNat(x(V1,V2))) | → | mark(U31(isNat(V1),V2)) | (15) |
active(U52(tt,M,N)) | → | mark(s(plus(N,M))) | (8) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
active(U11(tt,V2)) | → | mark(U12(isNat(V2))) | (1) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
active(U21(tt)) | → | mark(tt) | (3) |
active(plus(N,0)) | → | mark(U41(isNat(N),N)) | (16) |
mark(tt) | → | active(tt) | (21) |
mark(x(X1,X2)) | → | active(x(mark(X1),mark(X2))) | (36) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
mark(U32(X)) | → | active(U32(mark(X))) | (26) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
active(x(N,s(M))) | → | mark(U71(isNat(M),M,N)) | (19) |
mark(U61(X)) | → | active(U61(mark(X))) | (32) |
active(plus(N,s(M))) | → | mark(U51(isNat(M),M,N)) | (17) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
mark(U41(X1,X2)) | → | active(U41(mark(X1),X2)) | (27) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
mark(U71(X1,X2,X3)) | → | active(U71(mark(X1),X2,X3)) | (34) |
mark(U12(X)) | → | active(U12(mark(X))) | (22) |
mark(U51(X1,X2,X3)) | → | active(U51(mark(X1),X2,X3)) | (28) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
active(U32(tt)) | → | mark(tt) | (5) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
mark(0) | → | active(0) | (33) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
x(X1,active(X2)) | → | x(X1,X2) | (92) |
active(U71(tt,M,N)) | → | mark(U72(isNat(N),M,N)) | (10) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
active(U51(tt,M,N)) | → | mark(U52(isNat(N),M,N)) | (7) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
mark(U11(X1,X2)) | → | active(U11(mark(X1),X2)) | (20) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (25) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
mark(s(X)) | → | active(s(mark(X))) | (30) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
active(isNat(s(V1))) | → | mark(U21(isNat(V1))) | (14) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
x(mark(X1),X2) | → | x(X1,X2) | (89) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (31) |
active(isNat(0)) | → | mark(tt) | (12) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
mark(isNat(X)) | → | active(isNat(X)) | (23) |
s(active(X)) | → | s(X) | (70) |
mark(U21(X)) | → | active(U21(mark(X))) | (24) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
active(U72(tt,M,N)) | → | mark(plus(x(N,M),N)) | (11) |
active(U61(tt)) | → | mark(0) | (9) |
active(isNat(plus(V1,V2))) | → | mark(U11(isNat(V1),V2)) | (13) |
U32(mark(X)) | → | U32(X) | (51) |
x(X1,mark(X2)) | → | x(X1,X2) | (90) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
active(U41(tt,N)) | → | mark(N) | (6) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
x(active(X1),X2) | → | x(X1,X2) | (91) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
mark(U72(X1,X2,X3)) | → | active(U72(mark(X1),X2,X3)) | (35) |
mark(U52(X1,X2,X3)) | → | active(U52(mark(X1),X2,X3)) | (29) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
active(U12(tt)) | → | mark(tt) | (2) |
active#(U51(tt,M,N)) | → | mark#(U52(isNat(N),M,N)) | (224) |
The dependency pairs are split into 1 component.
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (234) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
mark#(U51(X1,X2,X3)) | → | active#(U51(mark(X1),X2,X3)) | (109) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
active#(U41(tt,N)) | → | mark#(N) | (200) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 7 |
[U11(x1, x2)] | = | x2 + 7 |
[s(x1)] | = | 8 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | 5 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | 0 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 9 |
[x(x1, x2)] | = | 2 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 48032 |
[0] | = | 6 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 3 |
[U32(x1)] | = | 9 |
[isNat(x1)] | = | 5 |
[U52(x1, x2, x3)] | = | x3 + 6 |
[plus(x1, x2)] | = | 2 |
[U61(x1)] | = | 4 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 4 |
[U31(x1, x2)] | = | 7 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | x1 + 48027 |
[U21#(x1)] | = | 0 |
[tt] | = | 11 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | 4 |
[U41(x1, x2)] | = | 5 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
x(X1,active(X2)) | → | x(X1,X2) | (92) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
x(mark(X1),X2) | → | x(X1,X2) | (89) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
s(active(X)) | → | s(X) | (70) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
U32(mark(X)) | → | U32(X) | (51) |
x(X1,mark(X2)) | → | x(X1,X2) | (90) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
x(active(X1),X2) | → | x(X1,X2) | (91) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
mark#(U51(X1,X2,X3)) | → | active#(U51(mark(X1),X2,X3)) | (109) |
The dependency pairs are split into 1 component.
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (234) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
active#(U41(tt,N)) | → | mark#(N) | (200) |
π(U72#) | = | 1 |
π(U21) | = | 1 |
π(U11) | = | 1 |
π(plus#) | = | 1 |
π(U12) | = | 1 |
π(mark#) | = | 1 |
π(x#) | = | 1 |
π(s#) | = | 1 |
π(mark) | = | 1 |
π(U11#) | = | 2 |
π(active) | = | 1 |
π(U31) | = | 1 |
π(active#) | = | 1 |
π(U21#) | = | 1 |
π(U71#) | = | 1 |
prec(U32#) | = | 0 | status(U32#) | = | [] | list-extension(U32#) | = | Lex | ||
prec(s) | = | 2 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(isNat#) | = | 0 | status(isNat#) | = | [] | list-extension(isNat#) | = | Lex | ||
prec(U71) | = | 4 | status(U71) | = | [2, 3, 1] | list-extension(U71) | = | Lex | ||
prec(U72) | = | 4 | status(U72) | = | [2, 3, 1] | list-extension(U72) | = | Lex | ||
prec(U52#) | = | 0 | status(U52#) | = | [3, 2] | list-extension(U52#) | = | Lex | ||
prec(x) | = | 4 | status(x) | = | [2, 1] | list-extension(x) | = | Lex | ||
prec(U12#) | = | 0 | status(U12#) | = | [] | list-extension(U12#) | = | Lex | ||
prec(0) | = | 1 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(U32) | = | 1 | status(U32) | = | [] | list-extension(U32) | = | Lex | ||
prec(isNat) | = | 1 | status(isNat) | = | [] | list-extension(isNat) | = | Lex | ||
prec(U52) | = | 3 | status(U52) | = | [3, 2, 1] | list-extension(U52) | = | Lex | ||
prec(plus) | = | 3 | status(plus) | = | [1, 2] | list-extension(plus) | = | Lex | ||
prec(U61) | = | 4 | status(U61) | = | [1] | list-extension(U61) | = | Lex | ||
prec(U51#) | = | 0 | status(U51#) | = | [3, 2, 1] | list-extension(U51#) | = | Lex | ||
prec(U41#) | = | 0 | status(U41#) | = | [1, 2] | list-extension(U41#) | = | Lex | ||
prec(tt) | = | 1 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(U51) | = | 3 | status(U51) | = | [3, 2, 1] | list-extension(U51) | = | Lex | ||
prec(U41) | = | 3 | status(U41) | = | [2] | list-extension(U41) | = | Lex | ||
prec(U31#) | = | 0 | status(U31#) | = | [2, 1] | list-extension(U31#) | = | Lex | ||
prec(U61#) | = | 0 | status(U61#) | = | [] | list-extension(U61#) | = | Lex |
[U32#(x1)] | = | 0 |
[s(x1)] | = | x1 + 0 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U72(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U52#(x1, x2, x3)] | = | max(x2 + 0, x3 + 0, 0) |
[x(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U12#(x1)] | = | 0 |
[0] | = | 0 |
[U32(x1)] | = | 0 |
[isNat(x1)] | = | 0 |
[U52(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[plus(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U61(x1)] | = | x1 + 0 |
[U51#(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U41#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[tt] | = | 0 |
[U51(x1, x2, x3)] | = | max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U41(x1, x2)] | = | max(x2 + 0, 0) |
[U31#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[U61#(x1)] | = | 0 |
active(x(N,0)) | → | mark(U61(isNat(N))) | (18) |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
active(U31(tt,V2)) | → | mark(U32(isNat(V2))) | (4) |
active(isNat(x(V1,V2))) | → | mark(U31(isNat(V1),V2)) | (15) |
active(U52(tt,M,N)) | → | mark(s(plus(N,M))) | (8) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
active(U11(tt,V2)) | → | mark(U12(isNat(V2))) | (1) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
active(U21(tt)) | → | mark(tt) | (3) |
active(plus(N,0)) | → | mark(U41(isNat(N),N)) | (16) |
mark(tt) | → | active(tt) | (21) |
mark(x(X1,X2)) | → | active(x(mark(X1),mark(X2))) | (36) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
mark(U32(X)) | → | active(U32(mark(X))) | (26) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
active(x(N,s(M))) | → | mark(U71(isNat(M),M,N)) | (19) |
mark(U61(X)) | → | active(U61(mark(X))) | (32) |
active(plus(N,s(M))) | → | mark(U51(isNat(M),M,N)) | (17) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
mark(U41(X1,X2)) | → | active(U41(mark(X1),X2)) | (27) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
mark(U71(X1,X2,X3)) | → | active(U71(mark(X1),X2,X3)) | (34) |
mark(U12(X)) | → | active(U12(mark(X))) | (22) |
mark(U51(X1,X2,X3)) | → | active(U51(mark(X1),X2,X3)) | (28) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
active(U32(tt)) | → | mark(tt) | (5) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
mark(0) | → | active(0) | (33) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
x(X1,active(X2)) | → | x(X1,X2) | (92) |
active(U71(tt,M,N)) | → | mark(U72(isNat(N),M,N)) | (10) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
active(U51(tt,M,N)) | → | mark(U52(isNat(N),M,N)) | (7) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
mark(U11(X1,X2)) | → | active(U11(mark(X1),X2)) | (20) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (25) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
mark(s(X)) | → | active(s(mark(X))) | (30) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
active(isNat(s(V1))) | → | mark(U21(isNat(V1))) | (14) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
x(mark(X1),X2) | → | x(X1,X2) | (89) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (31) |
active(isNat(0)) | → | mark(tt) | (12) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
mark(isNat(X)) | → | active(isNat(X)) | (23) |
s(active(X)) | → | s(X) | (70) |
mark(U21(X)) | → | active(U21(mark(X))) | (24) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
active(U72(tt,M,N)) | → | mark(plus(x(N,M),N)) | (11) |
active(U61(tt)) | → | mark(0) | (9) |
active(isNat(plus(V1,V2))) | → | mark(U11(isNat(V1),V2)) | (13) |
U32(mark(X)) | → | U32(X) | (51) |
x(X1,mark(X2)) | → | x(X1,X2) | (90) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
active(U41(tt,N)) | → | mark(N) | (6) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
x(active(X1),X2) | → | x(X1,X2) | (91) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
mark(U72(X1,X2,X3)) | → | active(U72(mark(X1),X2,X3)) | (35) |
mark(U52(X1,X2,X3)) | → | active(U52(mark(X1),X2,X3)) | (29) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
active(U12(tt)) | → | mark(tt) | (2) |
active#(U41(tt,N)) | → | mark#(N) | (200) |
The dependency pairs are split into 1 component.
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (234) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 5539 |
[U11(x1, x2)] | = | 12229 |
[s(x1)] | = | 12229 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | 12227 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | 4908 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 12229 |
[x(x1, x2)] | = | 4037 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 60254 |
[0] | = | 12229 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | 12228 |
[U32(x1)] | = | 12229 |
[isNat(x1)] | = | 12227 |
[U52(x1, x2, x3)] | = | 1 |
[plus(x1, x2)] | = | 12229 |
[U61(x1)] | = | 12227 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | 1 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | x1 + 48027 |
[U21#(x1)] | = | 0 |
[tt] | = | 12229 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | 12227 |
[U41(x1, x2)] | = | 5656 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
x(X1,active(X2)) | → | x(X1,X2) | (92) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
x(mark(X1),X2) | → | x(X1,X2) | (89) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
s(active(X)) | → | s(X) | (70) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
U32(mark(X)) | → | U32(X) | (51) |
x(X1,mark(X2)) | → | x(X1,X2) | (90) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
x(active(X1),X2) | → | x(X1,X2) | (91) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
mark#(U41(X1,X2)) | → | active#(U41(mark(X1),X2)) | (234) |
The dependency pairs are split into 1 component.
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 0 |
[U11(x1, x2)] | = | x1 + 0 |
[s(x1)] | = | x1 + 16552 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x1 + x3 + 20350 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 0 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 36 |
[x(x1, x2)] | = | x2 + 3828 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 47995 |
[0] | = | 36803 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[U32(x1)] | = | x1 + 14625 |
[isNat(x1)] | = | 32 |
[U52(x1, x2, x3)] | = | x3 + 16586 |
[plus(x1, x2)] | = | 36 |
[U61(x1)] | = | 36801 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[U31(x1, x2)] | = | x2 + 34 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 48027 |
[U21#(x1)] | = | 0 |
[tt] | = | 34 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x2 + 38 |
[U41(x1, x2)] | = | 38 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
s(active(X)) | → | s(X) | (70) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
U32(mark(X)) | → | U32(X) | (51) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
mark#(U71(X1,X2,X3)) | → | active#(U71(mark(X1),X2,X3)) | (108) |
The dependency pairs are split into 1 component.
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 0 |
[U11(x1, x2)] | = | x1 + 0 |
[s(x1)] | = | x1 + 23201 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x1 + x3 + 14367 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | 830 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 40214 |
[x(x1, x2)] | = | x2 + 31374 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 47995 |
[0] | = | 41385 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[U32(x1)] | = | x1 + 23492 |
[isNat(x1)] | = | 40210 |
[U52(x1, x2, x3)] | = | x3 + 24031 |
[plus(x1, x2)] | = | 832 |
[U61(x1)] | = | 41383 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[U31(x1, x2)] | = | x2 + 40212 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 40212 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x2 + 834 |
[U41(x1, x2)] | = | 834 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U31(X1,active(X2)) | → | U31(X1,X2) | (50) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (80) |
U41(X1,mark(X2)) | → | U41(X1,X2) | (54) |
U71(mark(X1),X2,X3) | → | U71(X1,X2,X3) | (77) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (68) |
U72(X1,X2,mark(X3)) | → | U72(X1,X2,X3) | (85) |
U52(mark(X1),X2,X3) | → | U52(X1,X2,X3) | (63) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (60) |
U72(X1,active(X2),X3) | → | U72(X1,X2,X3) | (87) |
U72(X1,mark(X2),X3) | → | U72(X1,X2,X3) | (84) |
U52(X1,X2,mark(X3)) | → | U52(X1,X2,X3) | (65) |
isNat(active(X)) | → | isNat(X) | (44) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (72) |
U52(X1,mark(X2),X3) | → | U52(X1,X2,X3) | (64) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
U72(X1,X2,active(X3)) | → | U72(X1,X2,X3) | (88) |
U31(active(X1),X2) | → | U31(X1,X2) | (49) |
U32(active(X)) | → | U32(X) | (52) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (62) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (82) |
U41(X1,active(X2)) | → | U41(X1,X2) | (56) |
U71(X1,X2,mark(X3)) | → | U71(X1,X2,X3) | (79) |
s(mark(X)) | → | s(X) | (69) |
U21(mark(X)) | → | U21(X) | (45) |
U71(X1,mark(X2),X3) | → | U71(X1,X2,X3) | (78) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (81) |
s(active(X)) | → | s(X) | (70) |
U61(active(X)) | → | U61(X) | (76) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (57) |
U32(mark(X)) | → | U32(X) | (51) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (67) |
U41(active(X1),X2) | → | U41(X1,X2) | (55) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (59) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (61) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (58) |
plus(X1,active(X2)) | → | plus(X1,X2) | (74) |
U61(mark(X)) | → | U61(X) | (75) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (48) |
plus(mark(X1),X2) | → | plus(X1,X2) | (71) |
U41(mark(X1),X2) | → | U41(X1,X2) | (53) |
U31(mark(X1),X2) | → | U31(X1,X2) | (47) |
plus(active(X1),X2) | → | plus(X1,X2) | (73) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U21(active(X)) | → | U21(X) | (46) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (66) |
U72(mark(X1),X2,X3) | → | U72(X1,X2,X3) | (83) |
isNat(mark(X)) | → | isNat(X) | (43) |
U72(active(X1),X2,X3) | → | U72(X1,X2,X3) | (86) |
active#(U71(tt,M,N)) | → | mark#(U72(isNat(N),M,N)) | (151) |
The dependency pairs are split into 1 component.
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
[U72#(x1, x2, x3)] | = | max(0) |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 1 |
[U11(x1, x2)] | = | max(x1 + 1, x2 + 2, 0) |
[s(x1)] | = | x1 + 3 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | max(0) |
[plus#(x1, x2)] | = | max(0) |
[U72(x1, x2, x3)] | = | max(0) |
[U52#(x1, x2, x3)] | = | max(0) |
[U12(x1)] | = | 0 |
[x(x1, x2)] | = | max(0) |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | x1 + 1 |
[0] | = | 0 |
[x#(x1, x2)] | = | max(0) |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[U32(x1)] | = | 0 |
[isNat(x1)] | = | x1 + 4685 |
[U52(x1, x2, x3)] | = | max(0) |
[plus(x1, x2)] | = | max(x1 + 1172, x2 + 1145, 0) |
[U61(x1)] | = | 0 |
[U51#(x1, x2, x3)] | = | max(0) |
[U11#(x1, x2)] | = | max(0) |
[active(x1)] | = | x1 + 0 |
[U31(x1, x2)] | = | max(0) |
[U41#(x1, x2)] | = | max(0) |
[active#(x1)] | = | x1 + 0 |
[U21#(x1)] | = | 0 |
[tt] | = | 0 |
[U71#(x1, x2, x3)] | = | max(0) |
[U51(x1, x2, x3)] | = | max(0) |
[U41(x1, x2)] | = | max(0) |
[U31#(x1, x2)] | = | max(0) |
[U61#(x1)] | = | 0 |
isNat(active(X)) | → | isNat(X) | (44) |
U11(active(X1),X2) | → | U11(X1,X2) | (39) |
U21(mark(X)) | → | U21(X) | (45) |
U11(X1,active(X2)) | → | U11(X1,X2) | (40) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (38) |
U11(mark(X1),X2) | → | U11(X1,X2) | (37) |
U21(active(X)) | → | U21(X) | (46) |
isNat(mark(X)) | → | isNat(X) | (43) |
mark#(U11(X1,X2)) | → | mark#(X1) | (118) |
active#(isNat(s(V1))) | → | mark#(U21(isNat(V1))) | (124) |
mark#(isNat(X)) | → | active#(isNat(X)) | (111) |
mark#(U21(X)) | → | mark#(X) | (154) |
active#(isNat(plus(V1,V2))) | → | mark#(U11(isNat(V1),V2)) | (197) |
The dependency pairs are split into 0 components.
U21#(mark(X)) | → | U21#(X) | (239) |
U21#(active(X)) | → | U21#(X) | (158) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 2 |
[U11(x1, x2)] | = | x2 + 10183 |
[s(x1)] | = | x1 + 11419 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 23185 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 23186 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | x1 + 19725 |
[x(x1, x2)] | = | x2 + 11764 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 82942 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[U32(x1)] | = | x1 + 23605 |
[isNat(x1)] | = | 1 |
[U52(x1, x2, x3)] | = | x2 + 42840 |
[plus(x1, x2)] | = | 31423 |
[U61(x1)] | = | x1 + 57887 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + 15369 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | x1 + 0 |
[tt] | = | 8235 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x3 + 31425 |
[U41(x1, x2)] | = | 31425 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U21#(mark(X)) | → | U21#(X) | (239) |
U21#(active(X)) | → | U21#(X) | (158) |
The dependency pairs are split into 0 components.
U52#(X1,active(X2),X3) | → | U52#(X1,X2,X3) | (169) |
U52#(X1,mark(X2),X3) | → | U52#(X1,X2,X3) | (216) |
U52#(active(X1),X2,X3) | → | U52#(X1,X2,X3) | (140) |
U52#(X1,X2,mark(X3)) | → | U52#(X1,X2,X3) | (134) |
U52#(X1,X2,active(X3)) | → | U52#(X1,X2,X3) | (189) |
U52#(mark(X1),X2,X3) | → | U52#(X1,X2,X3) | (102) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 2 |
[U11(x1, x2)] | = | x2 + 24898 |
[s(x1)] | = | x1 + 15188 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 15191 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 15192 |
[U52#(x1, x2, x3)] | = | x1 + x3 + 0 |
[U12(x1)] | = | x1 + 38476 |
[x(x1, x2)] | = | x2 + 1 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 34663 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[U32(x1)] | = | x1 + 4 |
[isNat(x1)] | = | 1 |
[U52(x1, x2, x3)] | = | x2 + 30383 |
[plus(x1, x2)] | = | 15197 |
[U61(x1)] | = | x1 + 34658 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | 3 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 3 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x3 + 15199 |
[U41(x1, x2)] | = | 19811 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U52#(active(X1),X2,X3) | → | U52#(X1,X2,X3) | (140) |
U52#(X1,X2,mark(X3)) | → | U52#(X1,X2,X3) | (134) |
U52#(X1,X2,active(X3)) | → | U52#(X1,X2,X3) | (189) |
U52#(mark(X1),X2,X3) | → | U52#(X1,X2,X3) | (102) |
The dependency pairs are split into 1 component.
U52#(X1,mark(X2),X3) | → | U52#(X1,X2,X3) | (216) |
U52#(X1,active(X2),X3) | → | U52#(X1,X2,X3) | (169) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 2 |
[U11(x1, x2)] | = | x2 + 4421 |
[s(x1)] | = | x1 + 8349 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 8352 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 8353 |
[U52#(x1, x2, x3)] | = | x2 + 0 |
[U12(x1)] | = | x1 + 4422 |
[x(x1, x2)] | = | x2 + 1 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 6 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[U32(x1)] | = | x1 + 30974 |
[isNat(x1)] | = | 1 |
[U52(x1, x2, x3)] | = | x2 + 16705 |
[plus(x1, x2)] | = | 8358 |
[U61(x1)] | = | x1 + 1 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | 9462 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 3 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x3 + 8360 |
[U41(x1, x2)] | = | 12097 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U52#(X1,mark(X2),X3) | → | U52#(X1,X2,X3) | (216) |
U52#(X1,active(X2),X3) | → | U52#(X1,X2,X3) | (169) |
The dependency pairs are split into 0 components.
U11#(active(X1),X2) | → | U11#(X1,X2) | (238) |
U11#(mark(X1),X2) | → | U11#(X1,X2) | (232) |
U11#(X1,active(X2)) | → | U11#(X1,X2) | (159) |
U11#(X1,mark(X2)) | → | U11#(X1,X2) | (214) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 2 |
[U11(x1, x2)] | = | x2 + 3 |
[s(x1)] | = | x1 + 6 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 9 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 10 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | x1 + 4 |
[x(x1, x2)] | = | x2 + 1 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 39183 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[U32(x1)] | = | x1 + 40134 |
[isNat(x1)] | = | 1 |
[U52(x1, x2, x3)] | = | x2 + 19 |
[plus(x1, x2)] | = | 15 |
[U61(x1)] | = | x1 + 15338 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | x1 + x2 + 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | 29970 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 3 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x3 + 17 |
[U41(x1, x2)] | = | 17 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U11#(active(X1),X2) | → | U11#(X1,X2) | (238) |
U11#(mark(X1),X2) | → | U11#(X1,X2) | (232) |
U11#(X1,active(X2)) | → | U11#(X1,X2) | (159) |
U11#(X1,mark(X2)) | → | U11#(X1,X2) | (214) |
The dependency pairs are split into 0 components.
U51#(X1,active(X2),X3) | → | U51#(X1,X2,X3) | (172) |
U51#(X1,mark(X2),X3) | → | U51#(X1,X2,X3) | (146) |
U51#(active(X1),X2,X3) | → | U51#(X1,X2,X3) | (213) |
U51#(X1,X2,mark(X3)) | → | U51#(X1,X2,X3) | (194) |
U51#(X1,X2,active(X3)) | → | U51#(X1,X2,X3) | (186) |
U51#(mark(X1),X2,X3) | → | U51#(X1,X2,X3) | (104) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 24152 |
[U11(x1, x2)] | = | x2 + 15435 |
[s(x1)] | = | x1 + 21292 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 47142 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 39145 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | x1 + 7438 |
[x(x1, x2)] | = | x2 + 17218 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 75386 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[U32(x1)] | = | x1 + 21096 |
[isNat(x1)] | = | 7999 |
[U52(x1, x2, x3)] | = | x2 + 68438 |
[plus(x1, x2)] | = | 47148 |
[U61(x1)] | = | x1 + 53362 |
[U51#(x1, x2, x3)] | = | x2 + 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | 8001 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 8001 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x3 + 68436 |
[U41(x1, x2)] | = | 71135 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U51#(X1,active(X2),X3) | → | U51#(X1,X2,X3) | (172) |
U51#(X1,mark(X2),X3) | → | U51#(X1,X2,X3) | (146) |
The dependency pairs are split into 1 component.
U51#(active(X1),X2,X3) | → | U51#(X1,X2,X3) | (213) |
U51#(X1,X2,active(X3)) | → | U51#(X1,X2,X3) | (186) |
U51#(mark(X1),X2,X3) | → | U51#(X1,X2,X3) | (104) |
U51#(X1,X2,mark(X3)) | → | U51#(X1,X2,X3) | (194) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 17773 |
[U11(x1, x2)] | = | x2 + 3 |
[s(x1)] | = | x1 + 6 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 9 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 10 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | x1 + 4 |
[x(x1, x2)] | = | x2 + 1 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 45941 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[U32(x1)] | = | x1 + 4 |
[isNat(x1)] | = | 1 |
[U52(x1, x2, x3)] | = | x2 + 19 |
[plus(x1, x2)] | = | 15 |
[U61(x1)] | = | x1 + 45936 |
[U51#(x1, x2, x3)] | = | x1 + x3 + 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | 3 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 3 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x3 + 17 |
[U41(x1, x2)] | = | 17 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U51#(active(X1),X2,X3) | → | U51#(X1,X2,X3) | (213) |
U51#(X1,X2,active(X3)) | → | U51#(X1,X2,X3) | (186) |
U51#(mark(X1),X2,X3) | → | U51#(X1,X2,X3) | (104) |
U51#(X1,X2,mark(X3)) | → | U51#(X1,X2,X3) | (194) |
The dependency pairs are split into 0 components.
U71#(mark(X1),X2,X3) | → | U71#(X1,X2,X3) | (173) |
U71#(X1,mark(X2),X3) | → | U71#(X1,X2,X3) | (171) |
U71#(X1,X2,mark(X3)) | → | U71#(X1,X2,X3) | (142) |
U71#(X1,X2,active(X3)) | → | U71#(X1,X2,X3) | (204) |
U71#(active(X1),X2,X3) | → | U71#(X1,X2,X3) | (202) |
U71#(X1,active(X2),X3) | → | U71#(X1,X2,X3) | (116) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 9779 |
[U11(x1, x2)] | = | x1 + x2 + 13372 |
[s(x1)] | = | 72557 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 36895 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 3840 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 75340 |
[x(x1, x2)] | = | 36893 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 46476 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[U32(x1)] | = | x1 + 50635 |
[isNat(x1)] | = | 33057 |
[U52(x1, x2, x3)] | = | x1 + 39502 |
[plus(x1, x2)] | = | x1 + x2 + 2 |
[U61(x1)] | = | x1 + 13421 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x1 + x2 + 14318 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 33053 |
[U71#(x1, x2, x3)] | = | x1 + x2 + x3 + 0 |
[U51(x1, x2, x3)] | = | x1 + x3 + 39504 |
[U41(x1, x2)] | = | x1 + 13423 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U71#(mark(X1),X2,X3) | → | U71#(X1,X2,X3) | (173) |
U71#(X1,mark(X2),X3) | → | U71#(X1,X2,X3) | (171) |
U71#(X1,X2,mark(X3)) | → | U71#(X1,X2,X3) | (142) |
U71#(X1,X2,active(X3)) | → | U71#(X1,X2,X3) | (204) |
U71#(active(X1),X2,X3) | → | U71#(X1,X2,X3) | (202) |
U71#(X1,active(X2),X3) | → | U71#(X1,X2,X3) | (116) |
The dependency pairs are split into 0 components.
U12#(mark(X)) | → | U12#(X) | (166) |
U12#(active(X)) | → | U12#(X) | (138) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 15426 |
[U11(x1, x2)] | = | x1 + x2 + 2656 |
[s(x1)] | = | x1 + 51855 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 10207 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 93 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 26050 |
[x(x1, x2)] | = | 7551 |
[U12#(x1)] | = | x1 + 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 46476 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[U32(x1)] | = | 18082 |
[isNat(x1)] | = | 12770 |
[U52(x1, x2, x3)] | = | 65135 |
[plus(x1, x2)] | = | x1 + 15936 |
[U61(x1)] | = | x1 + 6523 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2656 |
[U31(x1, x2)] | = | x2 + 15426 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 20738 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x1 + x3 + 41741 |
[U41(x1, x2)] | = | x1 + 5822 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U32(active(X)) | → | U32(X) | (52) |
U32(mark(X)) | → | U32(X) | (51) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U12#(mark(X)) | → | U12#(X) | (166) |
U12#(active(X)) | → | U12#(X) | (138) |
The dependency pairs are split into 0 components.
U41#(X1,mark(X2)) | → | U41#(X1,X2) | (147) |
U41#(mark(X1),X2) | → | U41#(X1,X2) | (208) |
U41#(X1,active(X2)) | → | U41#(X1,X2) | (121) |
U41#(active(X1),X2) | → | U41#(X1,X2) | (96) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 11 |
[U11(x1, x2)] | = | x1 + x2 + 2656 |
[s(x1)] | = | x1 + 51855 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 11547 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 11540 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 2673 |
[x(x1, x2)] | = | 11545 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 46476 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[U32(x1)] | = | 13 |
[isNat(x1)] | = | 9 |
[U52(x1, x2, x3)] | = | 23229 |
[plus(x1, x2)] | = | x1 + 17 |
[U61(x1)] | = | x1 + 11538 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x2 + 11 |
[U41#(x1, x2)] | = | x1 + 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 15 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x1 + x3 + 6873 |
[U41(x1, x2)] | = | x1 + 10 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U32(active(X)) | → | U32(X) | (52) |
U32(mark(X)) | → | U32(X) | (51) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U41#(mark(X1),X2) | → | U41#(X1,X2) | (208) |
U41#(active(X1),X2) | → | U41#(X1,X2) | (96) |
The dependency pairs are split into 1 component.
U41#(X1,mark(X2)) | → | U41#(X1,X2) | (147) |
U41#(X1,active(X2)) | → | U41#(X1,X2) | (121) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 3 |
[U11(x1, x2)] | = | x1 + x2 + 21637 |
[s(x1)] | = | x1 + 1485 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 52684 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 52685 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 23119 |
[x(x1, x2)] | = | 33228 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 34711 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[U32(x1)] | = | 5 |
[isNat(x1)] | = | 1 |
[U52(x1, x2, x3)] | = | 22422 |
[plus(x1, x2)] | = | x1 + 20939 |
[U61(x1)] | = | x1 + 33229 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x2 + 3 |
[U41#(x1, x2)] | = | x2 + 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 1480 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x1 + x3 + 20940 |
[U41(x1, x2)] | = | x1 + 20940 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U32(active(X)) | → | U32(X) | (52) |
U32(mark(X)) | → | U32(X) | (51) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U41#(X1,mark(X2)) | → | U41#(X1,X2) | (147) |
U41#(X1,active(X2)) | → | U41#(X1,X2) | (121) |
The dependency pairs are split into 0 components.
s#(mark(X)) | → | s#(X) | (137) |
s#(active(X)) | → | s#(X) | (100) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 10746 |
[U11(x1, x2)] | = | x1 + x2 + 4098 |
[s(x1)] | = | x1 + 24588 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 9607 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 7057 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 27138 |
[x(x1, x2)] | = | 5509 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 34711 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | x1 + 0 |
[mark(x1)] | = | x1 + 1 |
[U32(x1)] | = | 14844 |
[isNat(x1)] | = | 6648 |
[U52(x1, x2, x3)] | = | 45078 |
[plus(x1, x2)] | = | x1 + 24588 |
[U61(x1)] | = | x1 + 2959 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 4098 |
[U31(x1, x2)] | = | x2 + 10746 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 18942 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x1 + x3 + 22038 |
[U41(x1, x2)] | = | x1 + 22038 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U32(active(X)) | → | U32(X) | (52) |
U32(mark(X)) | → | U32(X) | (51) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
s#(mark(X)) | → | s#(X) | (137) |
s#(active(X)) | → | s#(X) | (100) |
The dependency pairs are split into 0 components.
U31#(mark(X1),X2) | → | U31#(X1,X2) | (240) |
U31#(X1,active(X2)) | → | U31#(X1,X2) | (233) |
U31#(active(X1),X2) | → | U31#(X1,X2) | (156) |
U31#(X1,mark(X2)) | → | U31#(X1,X2) | (221) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 3 |
[U11(x1, x2)] | = | x1 + x2 + 31254 |
[s(x1)] | = | x1 + 15231 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 3 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 4 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 33437 |
[x(x1, x2)] | = | 1 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 34711 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 1 |
[U32(x1)] | = | 5 |
[isNat(x1)] | = | 1 |
[U52(x1, x2, x3)] | = | 22 |
[plus(x1, x2)] | = | x1 + 12 |
[U61(x1)] | = | x1 + 2 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 2 |
[U31(x1, x2)] | = | x2 + 3 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 7 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x1 + x3 + 13 |
[U41(x1, x2)] | = | x1 + 13 |
[U31#(x1, x2)] | = | x1 + x2 + 0 |
[U61#(x1)] | = | 0 |
U32(active(X)) | → | U32(X) | (52) |
U32(mark(X)) | → | U32(X) | (51) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U31#(mark(X1),X2) | → | U31#(X1,X2) | (240) |
U31#(X1,active(X2)) | → | U31#(X1,X2) | (233) |
U31#(active(X1),X2) | → | U31#(X1,X2) | (156) |
U31#(X1,mark(X2)) | → | U31#(X1,X2) | (221) |
The dependency pairs are split into 0 components.
U32#(active(X)) | → | U32#(X) | (218) |
U32#(mark(X)) | → | U32#(X) | (187) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | x1 + 0 |
[U21(x1)] | = | 21307 |
[U11(x1, x2)] | = | x1 + x2 + 2 |
[s(x1)] | = | x1 + 20646 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 21304 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 1 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 21315 |
[x(x1, x2)] | = | 2 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 61173 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 25058 |
[U32(x1)] | = | 21309 |
[isNat(x1)] | = | 21305 |
[U52(x1, x2, x3)] | = | 41956 |
[plus(x1, x2)] | = | x1 + 21312 |
[U61(x1)] | = | x1 + 39860 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 25059 |
[U31(x1, x2)] | = | x2 + 21307 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 21311 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x1 + x3 + 20643 |
[U41(x1, x2)] | = | x1 + 9 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U32(active(X)) | → | U32(X) | (52) |
U32(mark(X)) | → | U32(X) | (51) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U32#(active(X)) | → | U32#(X) | (218) |
U32#(mark(X)) | → | U32#(X) | (187) |
The dependency pairs are split into 0 components.
x#(active(X1),X2) | → | x#(X1,X2) | (222) |
x#(X1,mark(X2)) | → | x#(X1,X2) | (207) |
x#(mark(X1),X2) | → | x#(X1,X2) | (128) |
x#(X1,active(X2)) | → | x#(X1,X2) | (198) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 12 |
[U11(x1, x2)] | = | x1 + x2 + 27924 |
[s(x1)] | = | x1 + 12 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 23347 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 23339 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 27942 |
[x(x1, x2)] | = | 25 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 35 |
[x#(x1, x2)] | = | x1 + x2 + 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 25058 |
[U32(x1)] | = | 14 |
[isNat(x1)] | = | 10 |
[U52(x1, x2, x3)] | = | 23342 |
[plus(x1, x2)] | = | x1 + 23332 |
[U61(x1)] | = | x1 + 17 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 25059 |
[U31(x1, x2)] | = | x2 + 12 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 16 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x1 + x3 + 23324 |
[U41(x1, x2)] | = | x1 + 23324 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U32(active(X)) | → | U32(X) | (52) |
U32(mark(X)) | → | U32(X) | (51) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
x#(active(X1),X2) | → | x#(X1,X2) | (222) |
x#(X1,mark(X2)) | → | x#(X1,X2) | (207) |
x#(mark(X1),X2) | → | x#(X1,X2) | (128) |
x#(X1,active(X2)) | → | x#(X1,X2) | (198) |
The dependency pairs are split into 0 components.
U61#(mark(X)) | → | U61#(X) | (195) |
U61#(active(X)) | → | U61#(X) | (101) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 507 |
[U11(x1, x2)] | = | x1 + x2 + 2 |
[s(x1)] | = | x1 + 12 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 19745 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 19242 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 515 |
[x(x1, x2)] | = | 16816 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 42945 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 31874 |
[U32(x1)] | = | 509 |
[isNat(x1)] | = | 505 |
[U52(x1, x2, x3)] | = | 2949 |
[plus(x1, x2)] | = | x1 + 2939 |
[U61(x1)] | = | x1 + 16313 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 31875 |
[U31(x1, x2)] | = | x2 + 507 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 511 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x1 + x3 + 2436 |
[U41(x1, x2)] | = | x1 + 2436 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | x1 + 0 |
U32(active(X)) | → | U32(X) | (52) |
U32(mark(X)) | → | U32(X) | (51) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U61#(mark(X)) | → | U61#(X) | (195) |
U61#(active(X)) | → | U61#(X) | (101) |
The dependency pairs are split into 0 components.
isNat#(active(X)) | → | isNat#(X) | (162) |
isNat#(mark(X)) | → | isNat#(X) | (223) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 1345 |
[U11(x1, x2)] | = | x1 + x2 + 2 |
[s(x1)] | = | x1 + 12 |
[isNat#(x1)] | = | x1 + 0 |
[U71(x1, x2, x3)] | = | x3 + 19891 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 18550 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 1353 |
[x(x1, x2)] | = | 8558 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 42945 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 9141 |
[U32(x1)] | = | 1347 |
[isNat(x1)] | = | 1343 |
[U52(x1, x2, x3)] | = | 11353 |
[plus(x1, x2)] | = | x1 + 11343 |
[U61(x1)] | = | x1 + 7217 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 9142 |
[U31(x1, x2)] | = | x2 + 1345 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 1349 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x1 + x3 + 10002 |
[U41(x1, x2)] | = | x1 + 10002 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U32(active(X)) | → | U32(X) | (52) |
U32(mark(X)) | → | U32(X) | (51) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
isNat#(active(X)) | → | isNat#(X) | (162) |
isNat#(mark(X)) | → | isNat#(X) | (223) |
The dependency pairs are split into 0 components.
U72#(X1,active(X2),X3) | → | U72#(X1,X2,X3) | (157) |
U72#(X1,X2,active(X3)) | → | U72#(X1,X2,X3) | (143) |
U72#(X1,mark(X2),X3) | → | U72#(X1,X2,X3) | (215) |
U72#(X1,X2,mark(X3)) | → | U72#(X1,X2,X3) | (184) |
U72#(mark(X1),X2,X3) | → | U72#(X1,X2,X3) | (182) |
U72#(active(X1),X2,X3) | → | U72#(X1,X2,X3) | (93) |
[U72#(x1, x2, x3)] | = | x1 + x2 + 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | 3 |
[U11(x1, x2)] | = | x1 + x2 + 2 |
[s(x1)] | = | x1 + 1354 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x3 + 24018 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x1 + 24019 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 11 |
[x(x1, x2)] | = | 6283 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 42945 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 22284 |
[U32(x1)] | = | 5 |
[isNat(x1)] | = | 1 |
[U52(x1, x2, x3)] | = | 17755 |
[plus(x1, x2)] | = | x1 + 17745 |
[U61(x1)] | = | x1 + 26040 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 22285 |
[U31(x1, x2)] | = | x2 + 3 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 7 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x1 + x3 + 17746 |
[U41(x1, x2)] | = | x1 + 17746 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U32(active(X)) | → | U32(X) | (52) |
U32(mark(X)) | → | U32(X) | (51) |
U12(mark(X)) | → | U12(X) | (41) |
U12(active(X)) | → | U12(X) | (42) |
U72#(X1,active(X2),X3) | → | U72#(X1,X2,X3) | (157) |
U72#(X1,mark(X2),X3) | → | U72#(X1,X2,X3) | (215) |
U72#(mark(X1),X2,X3) | → | U72#(X1,X2,X3) | (182) |
U72#(active(X1),X2,X3) | → | U72#(X1,X2,X3) | (93) |
The dependency pairs are split into 1 component.
U72#(X1,X2,mark(X3)) | → | U72#(X1,X2,X3) | (184) |
U72#(X1,X2,active(X3)) | → | U72#(X1,X2,X3) | (143) |
[U72#(x1, x2, x3)] | = | x3 + 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 12605 |
[U11(x1, x2)] | = | x1 + x2 + 15366 |
[s(x1)] | = | x1 + 32209 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x1 + x3 + 26063 |
[plus#(x1, x2)] | = | 0 |
[U72(x1, x2, x3)] | = | x3 + 31739 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | x1 + 7688 |
[x(x1, x2)] | = | x1 + 3 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 25057 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 52474 |
[U32(x1)] | = | 6283 |
[isNat(x1)] | = | 2238 |
[U52(x1, x2, x3)] | = | x1 + x2 + 3669 |
[plus(x1, x2)] | = | 1 |
[U61(x1)] | = | x1 + 11430 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[U31(x1, x2)] | = | x1 + 5839 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 1 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x3 + 23748 |
[U41(x1, x2)] | = | 52472 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U72#(X1,X2,mark(X3)) | → | U72#(X1,X2,X3) | (184) |
U72#(X1,X2,active(X3)) | → | U72#(X1,X2,X3) | (143) |
The dependency pairs are split into 0 components.
plus#(X1,active(X2)) | → | plus#(X1,X2) | (149) |
plus#(active(X1),X2) | → | plus#(X1,X2) | (206) |
plus#(X1,mark(X2)) | → | plus#(X1,X2) | (199) |
plus#(mark(X1),X2) | → | plus#(X1,X2) | (176) |
[U72#(x1, x2, x3)] | = | 0 |
[U32#(x1)] | = | 0 |
[U21(x1)] | = | x1 + 9596 |
[U11(x1, x2)] | = | x2 + 85 |
[s(x1)] | = | x1 + 1 |
[isNat#(x1)] | = | 0 |
[U71(x1, x2, x3)] | = | x1 + x3 + 7192 |
[plus#(x1, x2)] | = | x1 + x2 + 0 |
[U72(x1, x2, x3)] | = | x1 + x3 + 3577 |
[U52#(x1, x2, x3)] | = | 0 |
[U12(x1)] | = | 5447 |
[x(x1, x2)] | = | x1 + 1083 |
[U12#(x1)] | = | 0 |
[mark#(x1)] | = | 88205 |
[0] | = | 14181 |
[x#(x1, x2)] | = | 0 |
[s#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 24077 |
[U32(x1)] | = | 10708 |
[isNat(x1)] | = | 1 |
[U52(x1, x2, x3)] | = | x1 + 25646 |
[plus(x1, x2)] | = | x2 + 11745 |
[U61(x1)] | = | 6794 |
[U51#(x1, x2, x3)] | = | 0 |
[U11#(x1, x2)] | = | 0 |
[active(x1)] | = | x1 + 1 |
[U31(x1, x2)] | = | 8743 |
[U41#(x1, x2)] | = | 0 |
[active#(x1)] | = | 88205 |
[U21#(x1)] | = | 0 |
[tt] | = | 1 |
[U71#(x1, x2, x3)] | = | 0 |
[U51(x1, x2, x3)] | = | x1 + x3 + 5513 |
[U41(x1, x2)] | = | 1851 |
[U31#(x1, x2)] | = | 0 |
[U61#(x1)] | = | 0 |
U32(active(X)) | → | U32(X) | (52) |
U61(active(X)) | → | U61(X) | (76) |
U32(mark(X)) | → | U32(X) | (51) |
U61(mark(X)) | → | U61(X) | (75) |
plus#(X1,active(X2)) | → | plus#(X1,X2) | (149) |
plus#(active(X1),X2) | → | plus#(X1,X2) | (206) |
plus#(X1,mark(X2)) | → | plus#(X1,X2) | (199) |
plus#(mark(X1),X2) | → | plus#(X1,X2) | (176) |
The dependency pairs are split into 0 components.