YES
Termination Proof using AProVETerm Rewriting System R:
[X, Y, Z, V, V1, V2, I, P]
((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
and(tt, X) -> X
isList(V) -> isNeList(V)
isList(nil) -> tt
isList((V1, V2)) -> and(isList(V1), isList(V2))
isNeList(V) -> isQid(V)
isNeList((V1, V2)) -> and(isList(V1), isNeList(V2))
isNeList((V1, V2)) -> and(isNeList(V1), isList(V2))
isNePal(V) -> isQid(V)
isNePal((I, (P, I))) -> and(isQid(I), isPal(P))
isPal(V) -> isNePal(V)
isPal(nil) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> tt
Termination of R to be shown.
TRS
↳CSR to TRS Transformation
Trivial-Transformation successful.
Replacement map:
and(1, 2)
(1, 2)
isPal(1)
isNePal(1)
isList(1)
isQid(1)
isNeList(1)
Old CSR:
((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
and(tt, X) -> X
isList(V) -> isNeList(V)
isList(nil) -> tt
isList((V1, V2)) -> and(isList(V1), isList(V2))
isNeList(V) -> isQid(V)
isNeList((V1, V2)) -> and(isList(V1), isNeList(V2))
isNeList((V1, V2)) -> and(isNeList(V1), isList(V2))
isNePal(V) -> isQid(V)
isNePal((I, (P, I))) -> and(isQid(I), isPal(P))
isPal(V) -> isNePal(V)
isPal(nil) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> tt
new TRS:
((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
and(tt, X) -> X
isList(V) -> isNeList(V)
isList(nil) -> tt
isList((V1, V2)) -> and(isList(V1), isList(V2))
isNeList(V) -> isQid(V)
isNeList((V1, V2)) -> and(isList(V1), isNeList(V2))
isNeList((V1, V2)) -> and(isNeList(V1), isList(V2))
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> tt
isNePal(V) -> isQid(V)
isNePal((I, (P, I))) -> and(isQid(I), isPal(P))
isPal(V) -> isNePal(V)
isPal(nil) -> tt
TRS
↳CSRtoTRS
→TRS1
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
isList((V1, V2)) -> and(isList(V1), isList(V2))
isNeList((V1, V2)) -> and(isList(V1), isNeList(V2))
isNeList((V1, V2)) -> and(isNeList(V1), isList(V2))
isNePal((I, (P, I))) -> and(isQid(I), isPal(P))
where the Polynomial interpretation:
| POL(and(x1, x2)) | = x1 + x2 |
| POL(i) | = 0 |
| POL(e) | = 0 |
| POL(__(x1, x2)) | = 1 + 2·x1 + x2 |
| POL(u) | = 0 |
| POL(isPal(x1)) | = x1 |
| POL(tt) | = 0 |
| POL(o) | = 0 |
| POL(nil) | = 0 |
| POL(isNePal(x1)) | = x1 |
| POL(isList(x1)) | = x1 |
| POL(a) | = 0 |
| POL(isQid(x1)) | = x1 |
| POL(isNeList(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:
isQid(a) -> tt
where the Polynomial interpretation:
| POL(and(x1, x2)) | = x1 + x2 |
| POL(i) | = 0 |
| POL(e) | = 0 |
| POL(u) | = 0 |
| POL(isPal(x1)) | = x1 |
| POL(tt) | = 0 |
| POL(o) | = 0 |
| POL(nil) | = 0 |
| POL(isNePal(x1)) | = x1 |
| POL(isList(x1)) | = x1 |
| POL(a) | = 1 |
| POL(isQid(x1)) | = x1 |
| POL(isNeList(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
...
→TRS3
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
isList(V) -> isNeList(V)
isList(nil) -> tt
where the Polynomial interpretation:
| POL(isPal(x1)) | = x1 |
| POL(and(x1, x2)) | = x1 + x2 |
| POL(i) | = 0 |
| POL(e) | = 0 |
| POL(tt) | = 0 |
| POL(o) | = 0 |
| POL(nil) | = 0 |
| POL(isNePal(x1)) | = x1 |
| POL(isList(x1)) | = 1 + x1 |
| POL(u) | = 0 |
| POL(isNeList(x1)) | = x1 |
| POL(isQid(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
...
→TRS4
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
isPal(nil) -> tt
where the Polynomial interpretation:
| POL(isPal(x1)) | = x1 |
| POL(and(x1, x2)) | = x1 + x2 |
| POL(i) | = 0 |
| POL(e) | = 0 |
| POL(tt) | = 0 |
| POL(o) | = 0 |
| POL(nil) | = 1 |
| POL(isNePal(x1)) | = x1 |
| POL(u) | = 0 |
| POL(isQid(x1)) | = x1 |
| POL(isNeList(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:
isPal(V) -> isNePal(V)
where the Polynomial interpretation:
| POL(and(x1, x2)) | = x1 + x2 |
| POL(isPal(x1)) | = 1 + x1 |
| POL(i) | = 0 |
| POL(e) | = 0 |
| POL(tt) | = 0 |
| POL(o) | = 0 |
| POL(isNePal(x1)) | = x1 |
| POL(u) | = 0 |
| POL(isQid(x1)) | = x1 |
| POL(isNeList(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:
and(tt, X) -> X
where the Polynomial interpretation:
| POL(and(x1, x2)) | = 1 + x1 + x2 |
| POL(i) | = 0 |
| POL(e) | = 0 |
| POL(tt) | = 0 |
| POL(o) | = 0 |
| POL(isNePal(x1)) | = x1 |
| POL(u) | = 0 |
| POL(isQid(x1)) | = x1 |
| POL(isNeList(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:
isQid(e) -> tt
where the Polynomial interpretation:
| POL(i) | = 0 |
| POL(e) | = 1 |
| POL(tt) | = 0 |
| POL(o) | = 0 |
| POL(isNePal(x1)) | = x1 |
| POL(u) | = 0 |
| POL(isQid(x1)) | = x1 |
| POL(isNeList(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:
isQid(u) -> tt
where the Polynomial interpretation:
| POL(i) | = 0 |
| POL(tt) | = 0 |
| POL(o) | = 0 |
| POL(isNePal(x1)) | = x1 |
| POL(u) | = 1 |
| POL(isQid(x1)) | = x1 |
| POL(isNeList(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
...
→TRS9
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
isQid(i) -> tt
where the Polynomial interpretation:
| POL(i) | = 1 |
| POL(o) | = 0 |
| POL(tt) | = 0 |
| POL(isNePal(x1)) | = x1 |
| POL(isQid(x1)) | = x1 |
| POL(isNeList(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:
isNeList(V) -> isQid(V)
where the Polynomial interpretation:
| POL(o) | = 0 |
| POL(tt) | = 0 |
| POL(isNePal(x1)) | = x1 |
| POL(isQid(x1)) | = x1 |
| POL(isNeList(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:
isNePal(V) -> isQid(V)
where the Polynomial interpretation:
| POL(o) | = 0 |
| POL(tt) | = 0 |
| POL(isNePal(x1)) | = 1 + x1 |
| POL(isQid(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
...
→TRS12
↳Removing Redundant Rules
Removing the following rules from R which fullfill a polynomial ordering:
isQid(o) -> tt
where the Polynomial interpretation:
| POL(o) | = 0 |
| POL(tt) | = 0 |
| POL(isQid(x1)) | = 1 + x1 |
was used.
All Rules of R can be deleted.
TRS
↳CSRtoTRS
→TRS1
↳RRRPolo
→TRS2
↳RRRPolo
...
→TRS13
↳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
...
→TRS14
↳Dependency Pair Analysis
R contains no Dependency Pairs and therefore no SCCs.
Termination of R successfully shown.
Duration:
0:03 minutes