Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/LengthOfFiniteLists_nokinds_GM)

The rewrite relation of the following TRS is considered.

a__zeros → cons(0,zeros) (1)
a__U11(tt,L) → s(a__length(mark(L))) (2)
a__and(tt,X) → mark(X) (3)
a__isNat(0) → tt (4)
a__isNat(length(V1)) → a__isNatList(V1) (5)
a__isNat(s(V1)) → a__isNat(V1) (6)
a__isNatIList(V) → a__isNatList(V) (7)
a__isNatIList(zeros) → tt (8)
a__isNatIList(cons(V1,V2)) → a__and(a__isNat(V1),isNatIList(V2)) (9)
a__isNatList(nil) → tt (10)
a__isNatList(cons(V1,V2)) → a__and(a__isNat(V1),isNatList(V2)) (11)
a__length(nil) → 0 (12)
a__length(cons(N,L)) → a__U11(a__and(a__isNatList(L),isNat(N)),L) (13)
mark(zeros) → a__zeros (14)
mark(U11(X1,X2)) → a__U11(mark(X1),X2) (15)
mark(length(X)) → a__length(mark(X)) (16)
mark(and(X1,X2)) → a__and(mark(X1),X2) (17)
mark(isNat(X)) → a__isNat(X) (18)
mark(isNatList(X)) → a__isNatList(X) (19)
mark(isNatIList(X)) → a__isNatIList(X) (20)
mark(cons(X1,X2)) → cons(mark(X1),X2) (21)
mark(0) → 0 (22)
mark(tt) → tt (23)
mark(s(X)) → s(mark(X)) (24)
mark(nil) → nil (25)
a__zeros → zeros (26)
a__U11(X1,X2) → U11(X1,X2) (27)
a__length(X) → length(X) (28)
a__and(X1,X2) → and(X1,X2) (29)
a__isNat(X) → isNat(X) (30)
a__isNatList(X) → isNatList(X) (31)
a__isNatIList(X) → isNatIList(X) (32)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[U11(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 1 1
0 1 0
0 1 0
· x2 +
0 0 0
0 0 0
0 0 0
[tt] =
0 0 0
0 0 0
0 0 0
[nil] =
0 0 0
1 0 0
1 0 0
[s(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 0 0
1 0 0
1 0 0
· x1 +
1 1 1
1 1 1
1 1 1
· x2 +
0 0 0
0 0 0
0 0 0
[isNatList(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[and(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 1 1
0 1 1
· x2 +
0 0 0
0 0 0
0 0 0
[isNat(x1)] =
1 0 0
1 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__U11(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 1 1
0 1 0
0 1 0
· x2 +
0 0 0
0 0 0
0 0 0
[a__isNat(x1)] =
1 0 0
1 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__zeros] =
0 0 0
0 0 0
0 0 0
[a__length(x1)] =
1 1 1
1 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[isNatIList(x1)] =
1 1 0
1 1 0
1 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__isNatList(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[length(x1)] =
1 1 1
1 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__and(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 1 1
0 1 1
· x2 +
0 0 0
0 0 0
0 0 0
[a__isNatIList(x1)] =
1 1 0
1 1 0
1 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 0
0 0 1
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[zeros] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
a__isNatList(nil) → tt (10)
a__length(nil) → 0 (12)

1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[U11(x1, x2)] =
1 0 0
0 0 0
0 0 1
· x1 +
1 1 1
0 0 0
0 0 0
· x2 +
1 0 0
1 0 0
0 0 0
[tt] =
0 0 0
0 0 0
0 0 0
[nil] =
0 0 0
0 0 0
0 0 0
[s(x1)] =
1 0 1
0 1 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 0 0
1 0 1
0 0 1
· x1 +
1 0 1
1 1 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[isNatList(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[and(x1, x2)] =
1 0 0
1 0 1
0 0 1
· x1 +
1 0 1
0 1 1
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[isNat(x1)] =
1 0 0
1 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__U11(x1, x2)] =
1 0 0
0 0 0
0 0 1
· x1 +
1 1 1
0 0 0
0 0 0
· x2 +
1 0 0
1 0 0
0 0 0
[a__isNat(x1)] =
1 0 0
1 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__zeros] =
0 0 0
0 0 0
0 0 0
[a__length(x1)] =
1 1 0
0 0 0
0 0 1
· x1 +
1 0 0
1 0 0
0 0 0
[isNatIList(x1)] =
1 1 1
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__isNatList(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[length(x1)] =
1 1 0
0 0 0
0 0 1
· x1 +
1 0 0
1 0 0
0 0 0
[a__and(x1, x2)] =
1 0 0
1 0 1
0 0 1
· x1 +
1 0 1
0 1 1
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[a__isNatIList(x1)] =
1 1 1
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 1
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[zeros] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
a__isNat(length(V1)) → a__isNatList(V1) (5)

1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[U11(x1, x2)] =
1 1 0
0 0 0
0 0 0
· x1 +
1 1 0
0 0 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[tt] =
0 0 0
0 0 0
0 0 0
[nil] =
0 0 0
0 0 0
0 0 0
[s(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
1 0 0
[cons(x1, x2)] =
1 0 0
1 0 0
0 0 0
· x1 +
1 1 1
1 1 1
0 0 0
· x2 +
0 0 0
0 0 0
1 0 0
[isNatList(x1)] =
1 0 1
0 1 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[and(x1, x2)] =
1 0 0
0 1 0
0 0 0
· x1 +
1 0 1
0 1 0
0 0 0
· x2 +
0 0 0
0 0 0
1 0 0
[isNat(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__U11(x1, x2)] =
1 1 0
0 0 0
0 0 0
· x1 +
1 1 0
0 0 0
0 0 0
· x2 +
0 0 0
0 0 0
1 0 0
[a__isNat(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__zeros] =
0 0 0
0 0 0
1 0 0
[a__length(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[isNatIList(x1)] =
1 0 1
0 1 1
0 0 0
· x1 +
1 0 0
0 0 0
1 0 0
[a__isNatList(x1)] =
1 0 1
0 1 1
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[length(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__and(x1, x2)] =
1 0 0
0 1 0
0 0 0
· x1 +
1 0 1
0 1 0
0 0 0
· x2 +
0 0 0
0 0 0
1 0 0
[a__isNatIList(x1)] =
1 0 1
0 1 1
0 0 0
· x1 +
1 0 0
0 0 0
1 0 0
[mark(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[zeros] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
a__isNatIList(V) → a__isNatList(V) (7)
a__isNatIList(zeros) → tt (8)
a__isNatList(cons(V1,V2)) → a__and(a__isNat(V1),isNatList(V2)) (11)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[U11(x1, x2)] =
1 1 0
0 0 1
0 1 0
· x1 +
1 1 0
0 1 1
0 1 1
· x2 +
0 0 0
0 0 0
0 0 0
[tt] =
0 0 0
0 0 0
0 0 0
[nil] =
0 0 0
1 0 0
1 0 0
[s(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 1 0
0 0 1
0 1 0
· x1 +
1 0 0
1 1 1
1 1 1
· x2 +
0 0 0
0 0 0
0 0 0
[isNatList(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[and(x1, x2)] =
1 0 0
0 1 0
0 0 1
· x1 +
1 0 0
0 1 1
0 1 1
· x2 +
0 0 0
0 0 0
0 0 0
[isNat(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__U11(x1, x2)] =
1 1 0
0 0 1
0 1 0
· x1 +
1 1 1
0 1 1
0 1 1
· x2 +
0 0 0
0 0 0
0 0 0
[a__isNat(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__zeros] =
0 0 0
0 0 0
0 0 0
[a__length(x1)] =
1 1 0
0 0 1
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[isNatIList(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__isNatList(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[length(x1)] =
1 1 0
0 0 1
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__and(x1, x2)] =
1 0 0
0 1 0
0 0 1
· x1 +
1 1 0
0 1 1
0 1 1
· x2 +
0 0 0
0 0 0
0 0 0
[a__isNatIList(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 1 0
0 0 1
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[zeros] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
mark(nil) → nil (25)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[U11(x1, x2)] =
1 0 0
0 1 0
0 0 1
· x1 +
1 1 0
1 1 1
0 0 1
· x2 +
1 0 0
1 0 0
0 0 0
[tt] =
0 0 0
0 0 0
0 0 0
[s(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 1 1
1 1 1
1 0 1
· x1 +
1 1 0
1 0 1
1 0 1
· x2 +
0 0 0
0 0 0
0 0 0
[isNatList(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[and(x1, x2)] =
1 0 0
0 1 0
0 0 1
· x1 +
1 0 1
1 1 1
0 1 0
· x2 +
0 0 0
0 0 0
0 0 0
[isNat(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__U11(x1, x2)] =
1 0 0
0 1 0
0 0 1
· x1 +
1 1 1
1 1 1
1 0 1
· x2 +
1 0 0
1 0 0
1 0 0
[a__isNat(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__zeros] =
0 0 0
0 0 0
0 0 0
[a__length(x1)] =
1 0 1
1 0 1
0 1 0
· x1 +
1 0 0
1 0 0
1 0 0
[isNatIList(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__isNatList(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[length(x1)] =
1 0 1
1 0 1
0 1 0
· x1 +
1 0 0
1 0 0
1 0 0
[a__and(x1, x2)] =
1 0 0
0 1 0
0 0 1
· x1 +
1 0 1
1 1 1
0 1 0
· x2 +
0 0 0
0 0 0
0 0 0
[a__isNatIList(x1)] =
1 0 0
1 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 1
1 0 1
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[zeros] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
mark(length(X)) → a__length(mark(X)) (16)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[U11(x1, x2)] =
1 0 1
0 0 0
0 0 0
· x1 +
1 1 0
1 0 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[tt] =
1 0 0
0 0 0
0 0 0
[s(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 0 0
0 0 1
0 0 1
· x1 +
1 1 1
1 1 0
0 0 0
· x2 +
1 0 0
0 0 0
0 0 0
[isNatList(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[and(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
1 1 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[isNat(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[a__U11(x1, x2)] =
1 0 1
0 0 0
0 0 0
· x1 +
1 1 0
1 0 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[a__isNat(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[a__zeros] =
1 0 0
0 0 0
0 0 0
[a__length(x1)] =
1 1 0
1 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[isNatIList(x1)] =
1 0 1
1 1 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[a__isNatList(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[length(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__and(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
1 1 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[a__isNatIList(x1)] =
1 0 1
1 1 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[zeros] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
mark(isNat(X)) → a__isNat(X) (18)
mark(isNatList(X)) → a__isNatList(X) (19)
mark(isNatIList(X)) → a__isNatIList(X) (20)
mark(0) → 0 (22)
mark(tt) → tt (23)
a__zeros → zeros (26)

1.1.1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
a__U11#(tt,L) → mark#(L) (33)
a__U11#(tt,L) → a__length#(mark(L)) (34)
a__and#(tt,X) → mark#(X) (35)
a__isNat#(s(V1)) → a__isNat#(V1) (36)
a__isNatIList#(cons(V1,V2)) → a__isNat#(V1) (37)
a__isNatIList#(cons(V1,V2)) → a__and#(a__isNat(V1),isNatIList(V2)) (38)
a__length#(cons(N,L)) → a__isNatList#(L) (39)
a__length#(cons(N,L)) → a__and#(a__isNatList(L),isNat(N)) (40)
a__length#(cons(N,L)) → a__U11#(a__and(a__isNatList(L),isNat(N)),L) (41)
mark#(zeros) → a__zeros# (42)
mark#(U11(X1,X2)) → mark#(X1) (43)
mark#(U11(X1,X2)) → a__U11#(mark(X1),X2) (44)
mark#(and(X1,X2)) → mark#(X1) (45)
mark#(and(X1,X2)) → a__and#(mark(X1),X2) (46)
mark#(cons(X1,X2)) → mark#(X1) (47)
mark#(s(X)) → mark#(X) (48)

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.