YES Termination w.r.t. Q proof of Transformed_CSR_04_PALINDROME_nokinds_iGM.ari

Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS
↳1 QTRSRRRProof (⇔, 82 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 8 ms)
↳4 QTRS
↳5 QTRSRRRProof (⇔, 18 ms)
↳6 QTRS
↳7 QTRSRRRProof (⇔, 0 ms)
↳8 QTRS
↳9 RisEmptyProof (⇔, 0 ms)
↳10 YES

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(__(x1, x2)) = 2 + 2·x1 + x2   
POL(a) = 2   
POL(active(x1)) = x1   
POL(and(x1, x2)) = 1 + 2·x1 + x2   
POL(e) = 2   
POL(i) = 2   
POL(isList(x1)) = 1 + 2·x1   
POL(isNeList(x1)) = 2·x1   
POL(isNePal(x1)) = 2 + 2·x1   
POL(isPal(x1)) = 2 + 2·x1   
POL(isQid(x1)) = 2·x1   
POL(mark(x1)) = x1   
POL(nil) = 1   
POL(o) = 2   
POL(tt) = 2   
POL(u) = 1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)


(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(isNeList(V)) → mark(isQid(V))
active(isPal(V)) → mark(isNePal(V))
active(isQid(u)) → mark(tt)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(__(x1, x2)) = 2 + 2·x1 + x2   
POL(a) = 1   
POL(active(x1)) = x1   
POL(and(x1, x2)) = 1 + 2·x1 + x2   
POL(e) = 1   
POL(i) = 2   
POL(isList(x1)) = 1 + x1   
POL(isNeList(x1)) = 1 + 2·x1   
POL(isNePal(x1)) = 2·x1   
POL(isPal(x1)) = 1 + 2·x1   
POL(isQid(x1)) = 2·x1   
POL(mark(x1)) = x1   
POL(nil) = 2   
POL(o) = 1   
POL(tt) = 2   
POL(u) = 1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

active(isNeList(V)) → mark(isQid(V))
active(isPal(V)) → mark(isNePal(V))


(4) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(isQid(u)) → mark(tt)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(__(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(a) = 2   
POL(active(x1)) = 1 + x1   
POL(and(x1, x2)) = 2 + 2·x1 + x2   
POL(e) = 2   
POL(i) = 2   
POL(isList(x1)) = 2 + 2·x1   
POL(isNeList(x1)) = 2 + x1   
POL(isNePal(x1)) = 2 + x1   
POL(isPal(x1)) = 2 + x1   
POL(isQid(x1)) = 2 + x1   
POL(mark(x1)) = 2·x1   
POL(nil) = 1   
POL(o) = 2   
POL(tt) = 1   
POL(u) = 1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

active(isQid(u)) → mark(tt)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(active(X)) → isList(X)
isNeList(active(X)) → isNeList(X)
isQid(active(X)) → isQid(X)
isNePal(active(X)) → isNePal(X)
isPal(active(X)) → isPal(X)


(6) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(nil) → active(nil)
mark(tt) → active(tt)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)

Q is empty.

(7) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Knuth-Bendix order [KBO] with precedence:
isPal1 > u > isNePal1 > isQid1 > isNeList1 > _2 > nil > isList1 > mark1 > and2 > tt > active1

and weight map:

nil=1
tt=1
u=1
mark_1=1
active_1=1
isList_1=1
isNeList_1=1
isQid_1=1
isNePal_1=1
isPal_1=1
___2=0
and_2=0

The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

mark(nil) → active(nil)
mark(tt) → active(tt)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)


(8) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(9) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(10) YES