Certification Problem

Input (TPDB TRS_Innermost/Transformed_CSR_innermost_04/LengthOfFiniteLists_nokinds_noand_GM)

The rewrite relation of the following TRS is considered.

a__zeros → cons(0,zeros) (1)
a__U11(tt) → tt (2)
a__U21(tt) → tt (3)
a__U31(tt) → tt (4)
a__U41(tt,V2) → a__U42(a__isNatIList(V2)) (5)
a__U42(tt) → tt (6)
a__U51(tt,V2) → a__U52(a__isNatList(V2)) (7)
a__U52(tt) → tt (8)
a__U61(tt,L,N) → a__U62(a__isNat(N),L) (9)
a__U62(tt,L) → s(a__length(mark(L))) (10)
a__isNat(0) → tt (11)
a__isNat(length(V1)) → a__U11(a__isNatList(V1)) (12)
a__isNat(s(V1)) → a__U21(a__isNat(V1)) (13)
a__isNatIList(V) → a__U31(a__isNatList(V)) (14)
a__isNatIList(zeros) → tt (15)
a__isNatIList(cons(V1,V2)) → a__U41(a__isNat(V1),V2) (16)
a__isNatList(nil) → tt (17)
a__isNatList(cons(V1,V2)) → a__U51(a__isNat(V1),V2) (18)
a__length(nil) → 0 (19)
a__length(cons(N,L)) → a__U61(a__isNatList(L),L,N) (20)
mark(zeros) → a__zeros (21)
mark(U11(X)) → a__U11(mark(X)) (22)
mark(U21(X)) → a__U21(mark(X)) (23)
mark(U31(X)) → a__U31(mark(X)) (24)
mark(U41(X1,X2)) → a__U41(mark(X1),X2) (25)
mark(U42(X)) → a__U42(mark(X)) (26)
mark(isNatIList(X)) → a__isNatIList(X) (27)
mark(U51(X1,X2)) → a__U51(mark(X1),X2) (28)
mark(U52(X)) → a__U52(mark(X)) (29)
mark(isNatList(X)) → a__isNatList(X) (30)
mark(U61(X1,X2,X3)) → a__U61(mark(X1),X2,X3) (31)
mark(U62(X1,X2)) → a__U62(mark(X1),X2) (32)
mark(isNat(X)) → a__isNat(X) (33)
mark(length(X)) → a__length(mark(X)) (34)
mark(cons(X1,X2)) → cons(mark(X1),X2) (35)
mark(0) → 0 (36)
mark(tt) → tt (37)
mark(s(X)) → s(mark(X)) (38)
mark(nil) → nil (39)
a__zeros → zeros (40)
a__U11(X) → U11(X) (41)
a__U21(X) → U21(X) (42)
a__U31(X) → U31(X) (43)
a__U41(X1,X2) → U41(X1,X2) (44)
a__U42(X) → U42(X) (45)
a__isNatIList(X) → isNatIList(X) (46)
a__U51(X1,X2) → U51(X1,X2) (47)
a__U52(X) → U52(X) (48)
a__isNatList(X) → isNatList(X) (49)
a__U61(X1,X2,X3) → U61(X1,X2,X3) (50)
a__U62(X1,X2) → U62(X1,X2) (51)
a__isNat(X) → isNat(X) (52)
a__length(X) → length(X) (53)
The evaluation strategy is innermost.

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__zeros] = 0
[cons(x1, x2)] = 1 · x1 + 2 · x2
[0] = 0
[zeros] = 0
[a__U11(x1)] = 1 · x1
[tt] = 0
[a__U21(x1)] = 1 · x1
[a__U31(x1)] = 1 · x1
[a__U41(x1, x2)] = 1 · x1 + 2 · x2
[a__U42(x1)] = 2 · x1
[a__isNatIList(x1)] = 1 · x1
[a__U51(x1, x2)] = 1 · x1 + 2 · x2
[a__U52(x1)] = 2 · x1
[a__isNatList(x1)] = 1 · x1
[a__U61(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[a__U62(x1, x2)] = 1 · x1 + 1 · x2
[a__isNat(x1)] = 1 · x1
[s(x1)] = 1 · x1
[a__length(x1)] = 1 · x1
[mark(x1)] = 1 · x1
[length(x1)] = 1 · x1
[nil] = 1
[U11(x1)] = 1 · x1
[U21(x1)] = 1 · x1
[U31(x1)] = 1 · x1
[U41(x1, x2)] = 1 · x1 + 2 · x2
[U42(x1)] = 2 · x1
[isNatIList(x1)] = 1 · x1
[U51(x1, x2)] = 1 · x1 + 2 · x2
[U52(x1)] = 2 · x1
[isNatList(x1)] = 1 · x1
[U61(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[U62(x1, x2)] = 1 · x1 + 1 · x2
[isNat(x1)] = 1 · x1
all of the following rules can be deleted.
a__isNatList(nil) → tt (17)
a__length(nil) → 0 (19)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__zeros] = 0
[cons(x1, x2)] = 2 · x1 + 2 · x2
[0] = 0
[zeros] = 0
[a__U11(x1)] = 2 · x1
[tt] = 0
[a__U21(x1)] = 1 · x1
[a__U31(x1)] = 1 · x1
[a__U41(x1, x2)] = 1 · x1 + 2 · x2
[a__U42(x1)] = 2 · x1
[a__isNatIList(x1)] = 1 · x1
[a__U51(x1, x2)] = 1 · x1 + 2 · x2
[a__U52(x1)] = 2 · x1
[a__isNatList(x1)] = 1 · x1
[a__U61(x1, x2, x3)] = 1 + 2 · x1 + 2 · x2 + 2 · x3
[a__U62(x1, x2)] = 1 + 1 · x1 + 2 · x2
[a__isNat(x1)] = 2 · x1
[s(x1)] = 1 · x1
[a__length(x1)] = 1 + 2 · x1
[mark(x1)] = 1 · x1
[length(x1)] = 1 + 2 · x1
[U11(x1)] = 2 · x1
[U21(x1)] = 1 · x1
[U31(x1)] = 1 · x1
[U41(x1, x2)] = 1 · x1 + 2 · x2
[U42(x1)] = 2 · x1
[isNatIList(x1)] = 1 · x1
[U51(x1, x2)] = 1 · x1 + 2 · x2
[U52(x1)] = 2 · x1
[isNatList(x1)] = 1 · x1
[U61(x1, x2, x3)] = 1 + 2 · x1 + 2 · x2 + 2 · x3
[U62(x1, x2)] = 1 + 1 · x1 + 2 · x2
[isNat(x1)] = 2 · x1
[nil] = 0
all of the following rules can be deleted.
a__isNat(length(V1)) → a__U11(a__isNatList(V1)) (12)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__zeros] = 0
[cons(x1, x2)] = 2 · x1 + 2 · x2
[0] = 0
[zeros] = 0
[a__U11(x1)] = 2 · x1
[tt] = 0
[a__U21(x1)] = 1 · x1
[a__U31(x1)] = 1 + 1 · x1
[a__U41(x1, x2)] = 1 + 2 · x1 + 1 · x2
[a__U42(x1)] = 1 · x1
[a__isNatIList(x1)] = 1 + 1 · x1
[a__U51(x1, x2)] = 2 · x1 + 2 · x2
[a__U52(x1)] = 2 · x1
[a__isNatList(x1)] = 1 · x1
[a__U61(x1, x2, x3)] = 2 · x1 + 2 · x2 + 2 · x3
[a__U62(x1, x2)] = 2 · x1 + 2 · x2
[a__isNat(x1)] = 1 · x1
[s(x1)] = 1 · x1
[a__length(x1)] = 2 · x1
[mark(x1)] = 1 · x1
[U11(x1)] = 2 · x1
[U21(x1)] = 1 · x1
[U31(x1)] = 1 + 1 · x1
[U41(x1, x2)] = 1 + 2 · x1 + 1 · x2
[U42(x1)] = 1 · x1
[isNatIList(x1)] = 1 + 1 · x1
[U51(x1, x2)] = 2 · x1 + 2 · x2
[U52(x1)] = 2 · x1
[isNatList(x1)] = 1 · x1
[U61(x1, x2, x3)] = 2 · x1 + 2 · x2 + 2 · x3
[U62(x1, x2)] = 2 · x1 + 2 · x2
[isNat(x1)] = 1 · x1
[length(x1)] = 2 · x1
[nil] = 0
all of the following rules can be deleted.
a__U31(tt) → tt (4)
a__isNatIList(zeros) → tt (15)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__zeros] = 0
[cons(x1, x2)] = 2 · x1 + 2 · x2
[0] = 0
[zeros] = 0
[a__U11(x1)] = 1 + 1 · x1
[tt] = 0
[a__U21(x1)] = 1 · x1
[a__U41(x1, x2)] = 1 · x1 + 2 · x2
[a__U42(x1)] = 2 · x1
[a__isNatIList(x1)] = 1 · x1
[a__U51(x1, x2)] = 2 · x1 + 2 · x2
[a__U52(x1)] = 1 · x1
[a__isNatList(x1)] = 1 · x1
[a__U61(x1, x2, x3)] = 1 · x1 + 2 · x2 + 2 · x3
[a__U62(x1, x2)] = 1 · x1 + 2 · x2
[a__isNat(x1)] = 1 · x1
[s(x1)] = 1 · x1
[a__length(x1)] = 2 · x1
[mark(x1)] = 1 · x1
[a__U31(x1)] = 1 · x1
[U11(x1)] = 1 + 1 · x1
[U21(x1)] = 1 · x1
[U31(x1)] = 1 · x1
[U41(x1, x2)] = 1 · x1 + 2 · x2
[U42(x1)] = 2 · x1
[isNatIList(x1)] = 1 · x1
[U51(x1, x2)] = 2 · x1 + 2 · x2
[U52(x1)] = 1 · x1
[isNatList(x1)] = 1 · x1
[U61(x1, x2, x3)] = 1 · x1 + 2 · x2 + 2 · x3
[U62(x1, x2)] = 1 · x1 + 2 · x2
[isNat(x1)] = 1 · x1
[length(x1)] = 2 · x1
[nil] = 0
all of the following rules can be deleted.
a__U11(tt) → tt (2)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__zeros] = 0
[cons(x1, x2)] = 2 · x1 + 2 · x2
[0] = 0
[zeros] = 0
[a__U21(x1)] = 1 · x1
[tt] = 0
[a__U41(x1, x2)] = 1 + 2 · x1 + 2 · x2
[a__U42(x1)] = 1 · x1
[a__isNatIList(x1)] = 1 + 1 · x1
[a__U51(x1, x2)] = 2 · x1 + 2 · x2
[a__U52(x1)] = 1 · x1
[a__isNatList(x1)] = 1 · x1
[a__U61(x1, x2, x3)] = 2 · x1 + 2 · x2 + 2 · x3
[a__U62(x1, x2)] = 2 · x1 + 2 · x2
[a__isNat(x1)] = 1 · x1
[s(x1)] = 1 · x1
[a__length(x1)] = 2 · x1
[mark(x1)] = 1 · x1
[a__U31(x1)] = 1 · x1
[U11(x1)] = 1 · x1
[a__U11(x1)] = 1 · x1
[U21(x1)] = 1 · x1
[U31(x1)] = 1 · x1
[U41(x1, x2)] = 1 + 2 · x1 + 2 · x2
[U42(x1)] = 1 · x1
[isNatIList(x1)] = 1 + 1 · x1
[U51(x1, x2)] = 2 · x1 + 2 · x2
[U52(x1)] = 1 · x1
[isNatList(x1)] = 1 · x1
[U61(x1, x2, x3)] = 2 · x1 + 2 · x2 + 2 · x3
[U62(x1, x2)] = 2 · x1 + 2 · x2
[isNat(x1)] = 1 · x1
[length(x1)] = 2 · x1
[nil] = 0
all of the following rules can be deleted.
a__isNatIList(V) → a__U31(a__isNatList(V)) (14)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__zeros] = 1
[cons(x1, x2)] = 1 + 1 · x1 + 2 · x2
[0] = 0
[zeros] = 0
[a__U21(x1)] = 1 · x1
[tt] = 0
[a__U41(x1, x2)] = 1 · x1 + 2 · x2
[a__U42(x1)] = 1 · x1
[a__isNatIList(x1)] = 1 · x1
[a__U51(x1, x2)] = 1 · x1 + 1 · x2
[a__U52(x1)] = 1 · x1
[a__isNatList(x1)] = 1 · x1
[a__U61(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[a__U62(x1, x2)] = 1 + 1 · x1 + 1 · x2
[a__isNat(x1)] = 1 · x1
[s(x1)] = 1 · x1
[a__length(x1)] = 1 · x1
[mark(x1)] = 1 + 1 · x1
[U11(x1)] = 1 · x1
[a__U11(x1)] = 1 · x1
[U21(x1)] = 1 · x1
[U31(x1)] = 1 · x1
[a__U31(x1)] = 1 · x1
[U41(x1, x2)] = 1 · x1 + 2 · x2
[U42(x1)] = 1 · x1
[isNatIList(x1)] = 1 · x1
[U51(x1, x2)] = 1 · x1 + 1 · x2
[U52(x1)] = 1 · x1
[isNatList(x1)] = 1 · x1
[U61(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[U62(x1, x2)] = 1 + 1 · x1 + 1 · x2
[isNat(x1)] = 1 · x1
[length(x1)] = 1 · x1
[nil] = 1
all of the following rules can be deleted.
a__isNatIList(cons(V1,V2)) → a__U41(a__isNat(V1),V2) (16)
a__isNatList(cons(V1,V2)) → a__U51(a__isNat(V1),V2) (18)
mark(isNatIList(X)) → a__isNatIList(X) (27)
mark(isNatList(X)) → a__isNatList(X) (30)
mark(isNat(X)) → a__isNat(X) (33)
mark(0) → 0 (36)
mark(tt) → tt (37)
mark(nil) → nil (39)
a__zeros → zeros (40)

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__zeros] = 0
[cons(x1, x2)] = 2 · x1 + 2 · x2
[0] = 0
[zeros] = 0
[a__U21(x1)] = 1 · x1
[tt] = 1
[a__U41(x1, x2)] = 1 · x1 + 2 · x2
[a__U42(x1)] = 2 · x1
[a__isNatIList(x1)] = 1 · x1
[a__U51(x1, x2)] = 2 · x1 + 2 · x2
[a__U52(x1)] = 1 · x1
[a__isNatList(x1)] = 2 · x1
[a__U61(x1, x2, x3)] = 1 + 1 · x1 + 2 · x2 + 2 · x3
[a__U62(x1, x2)] = 1 · x1 + 2 · x2
[a__isNat(x1)] = 2 + 2 · x1
[s(x1)] = 1 · x1
[a__length(x1)] = 1 + 2 · x1
[mark(x1)] = 1 · x1
[U11(x1)] = 1 · x1
[a__U11(x1)] = 1 · x1
[U21(x1)] = 1 · x1
[U31(x1)] = 2 · x1
[a__U31(x1)] = 2 · x1
[U41(x1, x2)] = 1 · x1 + 2 · x2
[U42(x1)] = 2 · x1
[U51(x1, x2)] = 2 · x1 + 2 · x2
[U52(x1)] = 1 · x1
[U61(x1, x2, x3)] = 1 + 1 · x1 + 2 · x2 + 2 · x3
[U62(x1, x2)] = 1 · x1 + 2 · x2
[length(x1)] = 1 + 2 · x1
[isNatIList(x1)] = 1 · x1
[isNatList(x1)] = 2 · x1
[isNat(x1)] = 2 + 1 · x1
all of the following rules can be deleted.
a__U41(tt,V2) → a__U42(a__isNatIList(V2)) (5)
a__U42(tt) → tt (6)
a__U51(tt,V2) → a__U52(a__isNatList(V2)) (7)
a__isNat(0) → tt (11)

1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__zeros] = 0
[cons(x1, x2)] = 1 · x1 + 2 · x2
[0] = 0
[zeros] = 0
[a__U21(x1)] = 1 · x1
[tt] = 0
[a__U52(x1)] = 1 · x1
[a__U61(x1, x2, x3)] = 1 · x1 + 2 · x2 + 2 · x3
[a__U62(x1, x2)] = 2 · x1 + 2 · x2
[a__isNat(x1)] = 1 · x1
[s(x1)] = 1 · x1
[a__length(x1)] = 2 · x1
[mark(x1)] = 1 · x1
[a__isNatList(x1)] = 1 · x1
[U11(x1)] = 2 · x1
[a__U11(x1)] = 2 · x1
[U21(x1)] = 1 · x1
[U31(x1)] = 1 · x1
[a__U31(x1)] = 1 · x1
[U41(x1, x2)] = 1 · x1 + 2 · x2
[a__U41(x1, x2)] = 1 · x1 + 2 · x2
[U42(x1)] = 1 · x1
[a__U42(x1)] = 1 · x1
[U51(x1, x2)] = 2 · x1 + 2 · x2
[a__U51(x1, x2)] = 2 · x1 + 2 · x2
[U52(x1)] = 1 · x1
[U61(x1, x2, x3)] = 1 · x1 + 2 · x2 + 2 · x3
[U62(x1, x2)] = 2 · x1 + 2 · x2
[length(x1)] = 2 · x1
[a__isNatIList(x1)] = 1 + 2 · x1
[isNatIList(x1)] = 2 · x1
[isNatList(x1)] = 1 · x1
[isNat(x1)] = 1 · x1
all of the following rules can be deleted.
a__isNatIList(X) → isNatIList(X) (46)

1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__zeros] = 0
[cons(x1, x2)] = 2 · x1 + 2 · x2
[0] = 0
[zeros] = 0
[a__U21(x1)] = 1 · x1
[tt] = 2
[a__U52(x1)] = 1 + 2 · x1
[a__U61(x1, x2, x3)] = 1 + 2 · x1 + 2 · x2 + 2 · x3
[a__U62(x1, x2)] = 2 · x1 + 2 · x2
[a__isNat(x1)] = 1 + 1 · x1
[s(x1)] = 1 + 1 · x1
[a__length(x1)] = 2 + 2 · x1
[mark(x1)] = 1 · x1
[a__isNatList(x1)] = 1 · x1
[U11(x1)] = 2 · x1
[a__U11(x1)] = 2 · x1
[U21(x1)] = 1 · x1
[U31(x1)] = 1 · x1
[a__U31(x1)] = 1 · x1
[U41(x1, x2)] = 2 · x1 + 2 · x2
[a__U41(x1, x2)] = 2 · x1 + 2 · x2
[U42(x1)] = 2 · x1
[a__U42(x1)] = 2 · x1
[U51(x1, x2)] = 2 · x1 + 2 · x2
[a__U51(x1, x2)] = 2 · x1 + 2 · x2
[U52(x1)] = 1 + 2 · x1
[U61(x1, x2, x3)] = 1 + 2 · x1 + 2 · x2 + 2 · x3
[U62(x1, x2)] = 2 · x1 + 2 · x2
[length(x1)] = 2 + 2 · x1
[isNatList(x1)] = 1 · x1
[isNat(x1)] = 1 · x1
all of the following rules can be deleted.
a__U52(tt) → tt (8)
a__U61(tt,L,N) → a__U62(a__isNat(N),L) (9)
a__U62(tt,L) → s(a__length(mark(L))) (10)
a__isNat(s(V1)) → a__U21(a__isNat(V1)) (13)
a__length(cons(N,L)) → a__U61(a__isNatList(L),L,N) (20)
a__isNat(X) → isNat(X) (52)

1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__zeros] = 0
[cons(x1, x2)] = 1 · x1 + 1 · x2
[0] = 0
[zeros] = 0
[a__U21(x1)] = 1 · x1
[tt] = 0
[mark(x1)] = 2 · x1
[U11(x1)] = 1 · x1
[a__U11(x1)] = 1 · x1
[U21(x1)] = 1 · x1
[U31(x1)] = 1 · x1
[a__U31(x1)] = 1 · x1
[U41(x1, x2)] = 1 · x1 + 1 · x2
[a__U41(x1, x2)] = 1 · x1 + 2 · x2
[U42(x1)] = 1 · x1
[a__U42(x1)] = 1 · x1
[U51(x1, x2)] = 1 · x1 + 1 · x2
[a__U51(x1, x2)] = 1 · x1 + 2 · x2
[U52(x1)] = 1 · x1
[a__U52(x1)] = 1 · x1
[U61(x1, x2, x3)] = 1 · x1 + 2 · x2 + 2 · x3
[a__U61(x1, x2, x3)] = 1 · x1 + 2 · x2 + 2 · x3
[U62(x1, x2)] = 1 · x1 + 2 · x2
[a__U62(x1, x2)] = 1 · x1 + 2 · x2
[length(x1)] = 1 · x1
[a__length(x1)] = 1 · x1
[s(x1)] = 1 · x1
[a__isNatList(x1)] = 1 + 1 · x1
[isNatList(x1)] = 1 · x1
all of the following rules can be deleted.
a__isNatList(X) → isNatList(X) (49)

1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__zeros] = 2
[cons(x1, x2)] = 1 + 2 · x1 + 1 · x2
[0] = 0
[zeros] = 1
[a__U21(x1)] = 2 + 2 · x1
[tt] = 1
[mark(x1)] = 2 · x1
[U11(x1)] = 1 + 2 · x1
[a__U11(x1)] = 2 + 2 · x1
[U21(x1)] = 1 + 2 · x1
[U31(x1)] = 1 + 1 · x1
[a__U31(x1)] = 2 + 1 · x1
[U41(x1, x2)] = 1 + 1 · x1 + 2 · x2
[a__U41(x1, x2)] = 2 + 1 · x1 + 2 · x2
[U42(x1)] = 1 + 1 · x1
[a__U42(x1)] = 2 + 1 · x1
[U51(x1, x2)] = 1 + 1 · x1 + 2 · x2
[a__U51(x1, x2)] = 2 + 1 · x1 + 2 · x2
[U52(x1)] = 1 + 1 · x1
[a__U52(x1)] = 2 + 1 · x1
[U61(x1, x2, x3)] = 1 + 1 · x1 + 2 · x2 + 2 · x3
[a__U61(x1, x2, x3)] = 2 + 1 · x1 + 2 · x2 + 2 · x3
[U62(x1, x2)] = 1 + 1 · x1 + 2 · x2
[a__U62(x1, x2)] = 2 + 1 · x1 + 2 · x2
[length(x1)] = 1 + 2 · x1
[a__length(x1)] = 2 + 2 · x1
[s(x1)] = 1 + 2 · x1
all of the following rules can be deleted.
a__U21(tt) → tt (3)
mark(cons(X1,X2)) → cons(mark(X1),X2) (35)
mark(s(X)) → s(mark(X)) (38)
a__U11(X) → U11(X) (41)
a__U21(X) → U21(X) (42)
a__U31(X) → U31(X) (43)
a__U41(X1,X2) → U41(X1,X2) (44)
a__U42(X) → U42(X) (45)
a__U51(X1,X2) → U51(X1,X2) (47)
a__U52(X) → U52(X) (48)
a__U61(X1,X2,X3) → U61(X1,X2,X3) (50)
a__U62(X1,X2) → U62(X1,X2) (51)
a__length(X) → length(X) (53)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__zeros] = 2
[cons(x1, x2)] = 1 · x1 + 1 · x2
[0] = 0
[zeros] = 2
[mark(x1)] = 1 + 2 · x1
[U11(x1)] = 2 · x1
[a__U11(x1)] = 1 · x1
[U21(x1)] = 2 + 2 · x1
[a__U21(x1)] = 1 + 1 · x1
[U31(x1)] = 2 + 2 · x1
[a__U31(x1)] = 1 + 1 · x1
[U41(x1, x2)] = 2 + 2 · x1 + 2 · x2
[a__U41(x1, x2)] = 1 + 1 · x1 + 2 · x2
[U42(x1)] = 1 + 2 · x1
[a__U42(x1)] = 1 · x1
[U51(x1, x2)] = 2 + 2 · x1 + 2 · x2
[a__U51(x1, x2)] = 1 + 1 · x1 + 2 · x2
[U52(x1)] = 2 + 2 · x1
[a__U52(x1)] = 1 + 1 · x1
[U61(x1, x2, x3)] = 1 + 2 · x1 + 1 · x2 + 2 · x3
[a__U61(x1, x2, x3)] = 1 · x1 + 2 · x2 + 2 · x3
[U62(x1, x2)] = 2 + 2 · x1 + 1 · x2
[a__U62(x1, x2)] = 1 + 1 · x1 + 2 · x2
[length(x1)] = 2 + 2 · x1
[a__length(x1)] = 2 · x1
all of the following rules can be deleted.
mark(zeros) → a__zeros (21)
mark(U21(X)) → a__U21(mark(X)) (23)
mark(U31(X)) → a__U31(mark(X)) (24)
mark(U41(X1,X2)) → a__U41(mark(X1),X2) (25)
mark(U42(X)) → a__U42(mark(X)) (26)
mark(U51(X1,X2)) → a__U51(mark(X1),X2) (28)
mark(U52(X)) → a__U52(mark(X)) (29)
mark(U61(X1,X2,X3)) → a__U61(mark(X1),X2,X3) (31)
mark(U62(X1,X2)) → a__U62(mark(X1),X2) (32)
mark(length(X)) → a__length(mark(X)) (34)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[a__zeros] = 1
[cons(x1, x2)] = 1 · x1 + 1 · x2
[0] = 0
[zeros] = 0
[mark(x1)] = 2 · x1
[U11(x1)] = 2 · x1
[a__U11(x1)] = 1 · x1
all of the following rules can be deleted.
a__zeros → cons(0,zeros) (1)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(mark) = 2 weight(mark) = 2
prec(U11) = 0 weight(U11) = 1
prec(a__U11) = 1 weight(a__U11) = 1
all of the following rules can be deleted.
mark(U11(X)) → a__U11(mark(X)) (22)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.