YES
Termination Proof using AProVETerm Rewriting System R:
[L, X, V1, V, V2, N]
zeros -> cons(0, zeros)
U11(tt, L) -> s(length(L))
and(tt, X) -> X
isNat(0) -> tt
isNat(length(V1)) -> isNatList(V1)
isNat(s(V1)) -> isNat(V1)
isNatIList(V) -> isNatList(V)
isNatIList(zeros) -> tt
isNatIList(cons(V1, V2)) -> and(isNat(V1), isNatIList(V2))
isNatList(nil) -> tt
isNatList(cons(V1, V2)) -> and(isNat(V1), isNatList(V2))
length(nil) -> 0
length(cons(N, L)) -> U11(and(isNatList(L), isNat(N)), L)
Termination of R to be shown.
TRS
↳CSR to TRS Transformation
incomplete Giesl-Middeldorp-Transformation successful.
Replacement map:
and(1, 2)
isNatList(1)
cons(1, 2)
s(1)
U11(1, 2)
length(1)
isNatIList(1)
isNat(1)
Old CSR:
zeros -> cons(0, zeros)
U11(tt, L) -> s(length(L))
and(tt, X) -> X
isNat(0) -> tt
isNat(length(V1)) -> isNatList(V1)
isNat(s(V1)) -> isNat(V1)
isNatIList(V) -> isNatList(V)
isNatIList(zeros) -> tt
isNatIList(cons(V1, V2)) -> and(isNat(V1), isNatIList(V2))
isNatList(nil) -> tt
isNatList(cons(V1, V2)) -> and(isNat(V1), isNatList(V2))
length(nil) -> 0
length(cons(N, L)) -> U11(and(isNatList(L), isNat(N)), L)
new TRS:
zeros -> cons(0, zeros)
zeros -> zeros
U11(tt, L) -> s(length(mark(L)))
U11(x0, x1) -> U11(x0, x1)
length(nil) -> 0
length(cons(N, L)) -> U11(and(isNatList(L), isNat(N)), L)
length(x0) -> length(x0)
mark(and(x0, x1)) -> and(mark(x0), x1)
mark(isNatList(x0)) -> isNatList(x0)
mark(zeros) -> zeros
mark(U11(x0, x1)) -> U11(mark(x0), x1)
mark(length(x0)) -> length(mark(x0))
mark(isNatIList(x0)) -> isNatIList(x0)
mark(isNat(x0)) -> isNat(x0)
mark(cons(x0, x1)) -> cons(mark(x0), x1)
mark(0) -> 0
mark(tt) -> tt
mark(s(x0)) -> s(mark(x0))
mark(nil) -> nil
and(tt, X) -> mark(X)
and(x0, x1) -> and(x0, x1)
isNat(0) -> tt
isNat(length(V1)) -> isNatList(V1)
isNat(s(V1)) -> isNat(V1)
isNat(x0) -> isNat(x0)
isNatList(nil) -> tt
isNatList(cons(V1, V2)) -> and(isNat(V1), isNatList(V2))
isNatList(x0) -> isNatList(x0)
isNatIList(V) -> isNatList(V)
isNatIList(zeros) -> tt
isNatIList(cons(V1, V2)) -> and(isNat(V1), isNatIList(V2))
isNatIList(x0) -> isNatIList(x0)
TRS
↳CSRtoTRS
→TRS1
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
zeros -> cons(0, zeros)
zeros -> zeros
length(nil) -> 0
mark(isNatList(x0)) -> isNatList(x0)
mark(0) -> 0
mark(tt) -> tt
mark(nil) -> nil
isNat(length(V1)) -> isNatList(V1)
isNat(x0) -> isNat(x0)
isNatList(x0) -> isNatList(x0)
isNatIList(V) -> isNatList(V)
isNatIList(cons(V1, V2)) -> and(isNat(V1), isNatIList(V2))
isNatIList(x0) -> isNatIList(x0)
where the Polynomial interpretation:
| POL(and(x1, x2)) | = x1 + x2 |
| POL(isNatList(x1)) | = x1 |
| POL(_length_(x1)) | = x1 |
| POL(_isNatList_(x1)) | = 1 + x1 |
| POL(_isNat_(x1)) | = 2 + x1 |
| POL(_and_(x1, x2)) | = x1 + x2 |
| POL(*mark*(x1)) | = 2 + x1 |
| POL(U11(x1, x2)) | = x1 + x2 |
| POL(isNat(x1)) | = x1 |
| POL(_zeros_) | = 2 |
| POL(0) | = 0 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(cons(x1, x2)) | = 1 + x1 + 2·x2 |
| POL(tt) | = 2 |
| POL(nil) | = 1 |
| POL(s(x1)) | = x1 |
| POL(zeros) | = 0 |
| POL(length(x1)) | = x1 |
| POL(_isNatIList_(x1)) | = 2 + x1 |
| POL(isNatIList(x1)) | = x1 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
mark(isNatIList(x0)) -> isNatIList(x0)
where the Polynomial interpretation:
| POL(and(x1, x2)) | = x1 + x2 |
| POL(isNatList(x1)) | = x1 |
| POL(_isNatList_(x1)) | = x1 |
| POL(_length_(x1)) | = x1 |
| POL(_isNat_(x1)) | = x1 |
| POL(_and_(x1, x2)) | = x1 + x2 |
| POL(*mark*(x1)) | = x1 |
| POL(U11(x1, x2)) | = x1 + x2 |
| POL(isNat(x1)) | = x1 |
| POL(_zeros_) | = 0 |
| POL(0) | = 0 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(cons(x1, x2)) | = x1 + 2·x2 |
| POL(tt) | = 0 |
| POL(nil) | = 0 |
| POL(s(x1)) | = x1 |
| POL(zeros) | = 0 |
| POL(length(x1)) | = x1 |
| POL(_isNatIList_(x1)) | = x1 |
| POL(isNatIList(x1)) | = 1 + x1 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS3
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
and(tt, X) -> mark(X)
U11(tt, L) -> s(length(mark(L)))
where the Polynomial interpretation:
| POL(and(x1, x2)) | = x1 + x2 |
| POL(isNatList(x1)) | = x1 |
| POL(_isNatList_(x1)) | = x1 |
| POL(_length_(x1)) | = x1 |
| POL(_isNat_(x1)) | = x1 |
| POL(_and_(x1, x2)) | = x1 + x2 |
| POL(*mark*(x1)) | = x1 |
| POL(U11(x1, x2)) | = x1 + x2 |
| POL(isNat(x1)) | = x1 |
| POL(_zeros_) | = 0 |
| POL(0) | = 1 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(cons(x1, x2)) | = x1 + 2·x2 |
| POL(tt) | = 1 |
| POL(nil) | = 1 |
| POL(s(x1)) | = x1 |
| POL(zeros) | = 0 |
| POL(length(x1)) | = x1 |
| POL(_isNatIList_(x1)) | = 1 + x1 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS4
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
and(x0, x1) -> and(x0, x1)
mark(cons(x0, x1)) -> cons(mark(x0), x1)
where the Polynomial interpretation:
| POL(and(x1, x2)) | = 1 + x1 + x2 |
| POL(isNatList(x1)) | = x1 |
| POL(_isNatList_(x1)) | = x1 |
| POL(_length_(x1)) | = x1 |
| POL(_isNat_(x1)) | = x1 |
| POL(_and_(x1, x2)) | = 2 + x1 + x2 |
| POL(*mark*(x1)) | = 2·x1 |
| POL(U11(x1, x2)) | = x1 + x2 |
| POL(isNat(x1)) | = x1 |
| POL(_zeros_) | = 0 |
| POL(0) | = 0 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(cons(x1, x2)) | = 2 + x1 + 2·x2 |
| POL(tt) | = 0 |
| POL(nil) | = 0 |
| POL(s(x1)) | = x1 |
| POL(zeros) | = 0 |
| POL(length(x1)) | = x1 |
| POL(_isNatIList_(x1)) | = x1 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS5
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
mark(and(x0, x1)) -> and(mark(x0), x1)
where the Polynomial interpretation:
| POL(and(x1, x2)) | = 1 + x1 + x2 |
| POL(isNatList(x1)) | = x1 |
| POL(_length_(x1)) | = x1 |
| POL(_isNatList_(x1)) | = x1 |
| POL(_isNat_(x1)) | = x1 |
| POL(_and_(x1, x2)) | = x1 + x2 |
| POL(*mark*(x1)) | = x1 |
| POL(U11(x1, x2)) | = x1 + x2 |
| POL(isNat(x1)) | = x1 |
| POL(_zeros_) | = 0 |
| POL(0) | = 0 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(cons(x1, x2)) | = x1 + 2·x2 |
| POL(tt) | = 0 |
| POL(nil) | = 0 |
| POL(s(x1)) | = x1 |
| POL(zeros) | = 0 |
| POL(length(x1)) | = x1 |
| POL(_isNatIList_(x1)) | = x1 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS6
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
isNatList(cons(V1, V2)) -> and(isNat(V1), isNatList(V2))
length(cons(N, L)) -> U11(and(isNatList(L), isNat(N)), L)
where the Polynomial interpretation:
| POL(isNatList(x1)) | = x1 |
| POL(_isNatList_(x1)) | = x1 |
| POL(_length_(x1)) | = x1 |
| POL(_isNat_(x1)) | = x1 |
| POL(_and_(x1, x2)) | = x1 + x2 |
| POL(*mark*(x1)) | = x1 |
| POL(U11(x1, x2)) | = x1 + x2 |
| POL(isNat(x1)) | = x1 |
| POL(_zeros_) | = 0 |
| POL(0) | = 0 |
| POL(cons(x1, x2)) | = 1 + x1 + 2·x2 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(tt) | = 0 |
| POL(nil) | = 0 |
| POL(s(x1)) | = x1 |
| POL(zeros) | = 0 |
| POL(_isNatIList_(x1)) | = x1 |
| POL(length(x1)) | = x1 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS7
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
isNat(0) -> tt
where the Polynomial interpretation:
| POL(_length_(x1)) | = x1 |
| POL(_isNatList_(x1)) | = x1 |
| POL(_isNat_(x1)) | = x1 |
| POL(*mark*(x1)) | = x1 |
| POL(U11(x1, x2)) | = x1 + x2 |
| POL(isNat(x1)) | = x1 |
| POL(_zeros_) | = 0 |
| POL(0) | = 1 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(tt) | = 0 |
| POL(nil) | = 0 |
| POL(s(x1)) | = x1 |
| POL(zeros) | = 0 |
| POL(_isNatIList_(x1)) | = x1 |
| POL(length(x1)) | = x1 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS8
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
mark(length(x0)) -> length(mark(x0))
where the Polynomial interpretation:
| POL(_length_(x1)) | = 1 + x1 |
| POL(_isNatList_(x1)) | = x1 |
| POL(_isNat_(x1)) | = x1 |
| POL(*mark*(x1)) | = 2·x1 |
| POL(U11(x1, x2)) | = x1 + x2 |
| POL(isNat(x1)) | = x1 |
| POL(_zeros_) | = 0 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(tt) | = 0 |
| POL(nil) | = 0 |
| POL(s(x1)) | = x1 |
| POL(zeros) | = 0 |
| POL(_isNatIList_(x1)) | = x1 |
| POL(length(x1)) | = 1 + x1 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS9
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
length(x0) -> length(x0)
where the Polynomial interpretation:
| POL(_isNatList_(x1)) | = x1 |
| POL(_length_(x1)) | = 1 + x1 |
| POL(_isNat_(x1)) | = x1 |
| POL(*mark*(x1)) | = x1 |
| POL(U11(x1, x2)) | = x1 + x2 |
| POL(isNat(x1)) | = x1 |
| POL(_zeros_) | = 0 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(tt) | = 0 |
| POL(nil) | = 0 |
| POL(s(x1)) | = x1 |
| POL(zeros) | = 0 |
| POL(_isNatIList_(x1)) | = x1 |
| POL(length(x1)) | = x1 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS10
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
mark(isNat(x0)) -> isNat(x0)
where the Polynomial interpretation:
| POL(_zeros_) | = 0 |
| POL(_isNatList_(x1)) | = x1 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(_isNat_(x1)) | = x1 |
| POL(tt) | = 0 |
| POL(nil) | = 0 |
| POL(*mark*(x1)) | = x1 |
| POL(s(x1)) | = x1 |
| POL(zeros) | = 0 |
| POL(U11(x1, x2)) | = x1 + x2 |
| POL(_isNatIList_(x1)) | = x1 |
| POL(isNat(x1)) | = 1 + x1 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS11
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
isNatIList(zeros) -> tt
where the Polynomial interpretation:
| POL(_zeros_) | = 0 |
| POL(_isNatList_(x1)) | = x1 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(_isNat_(x1)) | = x1 |
| POL(tt) | = 0 |
| POL(nil) | = 0 |
| POL(*mark*(x1)) | = x1 |
| POL(s(x1)) | = x1 |
| POL(zeros) | = 0 |
| POL(U11(x1, x2)) | = x1 + x2 |
| POL(_isNatIList_(x1)) | = 1 + x1 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS12
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
mark(zeros) -> zeros
where the Polynomial interpretation:
| POL(_isNatList_(x1)) | = x1 |
| POL(_zeros_) | = 0 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(_isNat_(x1)) | = x1 |
| POL(tt) | = 0 |
| POL(nil) | = 0 |
| POL(*mark*(x1)) | = x1 |
| POL(s(x1)) | = x1 |
| POL(zeros) | = 1 |
| POL(U11(x1, x2)) | = x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS13
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
U11(x0, x1) -> U11(x0, x1)
where the Polynomial interpretation:
| POL(_isNatList_(x1)) | = x1 |
| POL(_U11_(x1, x2)) | = 2 + x1 + x2 |
| POL(_isNat_(x1)) | = x1 |
| POL(tt) | = 0 |
| POL(nil) | = 0 |
| POL(*mark*(x1)) | = 2·x1 |
| POL(s(x1)) | = x1 |
| POL(U11(x1, x2)) | = 1 + x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS14
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
mark(s(x0)) -> s(mark(x0))
isNat(s(V1)) -> isNat(V1)
where the Polynomial interpretation:
| POL(_isNatList_(x1)) | = x1 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(_isNat_(x1)) | = x1 |
| POL(tt) | = 0 |
| POL(nil) | = 0 |
| POL(*mark*(x1)) | = 2·x1 |
| POL(s(x1)) | = 1 + x1 |
| POL(U11(x1, x2)) | = x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS15
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
isNatList(nil) -> tt
where the Polynomial interpretation:
| POL(_isNatList_(x1)) | = x1 |
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(tt) | = 0 |
| POL(nil) | = 1 |
| POL(*mark*(x1)) | = x1 |
| POL(U11(x1, x2)) | = x1 + x2 |
was used.
Not all Rules of R can be deleted, so we still have to regard a part of R.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS16
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
mark(U11(x0, x1)) -> U11(mark(x0), x1)
where the Polynomial interpretation:
| POL(_U11_(x1, x2)) | = x1 + x2 |
| POL(*mark*(x1)) | = x1 |
| POL(U11(x1, x2)) | = 1 + x1 + x2 |
was used.
All Rules of R can be deleted.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS17
↳Overlay and local confluence Check
The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS18
↳Dependency Pair Analysis
R contains no Dependency Pairs and therefore no SCCs.
Termination of R successfully shown.
Duration:
0:06 minutes