(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(activate(V2)))
U92(tt) → tt
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X
Q is empty.
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Combined order from the following AFS and order.
__(
x1,
x2) =
__(
x1,
x2)
nil =
nil
U11(
x1,
x2) =
U11(
x1,
x2)
tt =
tt
U12(
x1,
x2) =
U12(
x1,
x2)
isPalListKind(
x1) =
isPalListKind(
x1)
activate(
x1) =
x1
U13(
x1) =
x1
isNeList(
x1) =
isNeList(
x1)
U21(
x1,
x2,
x3) =
U21(
x1,
x2,
x3)
U22(
x1,
x2,
x3) =
U22(
x1,
x2,
x3)
U23(
x1,
x2,
x3) =
U23(
x1,
x2,
x3)
U24(
x1,
x2,
x3) =
U24(
x1,
x2,
x3)
U25(
x1,
x2) =
U25(
x1,
x2)
isList(
x1) =
isList(
x1)
U26(
x1) =
x1
U31(
x1,
x2) =
U31(
x1,
x2)
U32(
x1,
x2) =
U32(
x1,
x2)
U33(
x1) =
U33(
x1)
isQid(
x1) =
x1
U41(
x1,
x2,
x3) =
U41(
x1,
x2,
x3)
U42(
x1,
x2,
x3) =
U42(
x1,
x2,
x3)
U43(
x1,
x2,
x3) =
U43(
x1,
x2,
x3)
U44(
x1,
x2,
x3) =
U44(
x1,
x2,
x3)
U45(
x1,
x2) =
U45(
x1,
x2)
U46(
x1) =
U46(
x1)
U51(
x1,
x2,
x3) =
U51(
x1,
x2,
x3)
U52(
x1,
x2,
x3) =
U52(
x1,
x2,
x3)
U53(
x1,
x2,
x3) =
U53(
x1,
x2,
x3)
U54(
x1,
x2,
x3) =
U54(
x1,
x2,
x3)
U55(
x1,
x2) =
U55(
x1,
x2)
U56(
x1) =
x1
U61(
x1,
x2) =
U61(
x1,
x2)
U62(
x1,
x2) =
U62(
x1,
x2)
U63(
x1) =
U63(
x1)
U71(
x1,
x2,
x3) =
U71(
x1,
x2,
x3)
U72(
x1,
x2) =
U72(
x1,
x2)
U73(
x1,
x2) =
U73(
x1,
x2)
isPal(
x1) =
isPal(
x1)
U74(
x1) =
U74(
x1)
U81(
x1,
x2) =
U81(
x1,
x2)
U82(
x1,
x2) =
U82(
x1,
x2)
U83(
x1) =
x1
isNePal(
x1) =
isNePal(
x1)
U91(
x1,
x2) =
U91(
x1,
x2)
U92(
x1) =
x1
n__nil =
n__nil
n____(
x1,
x2) =
n____(
x1,
x2)
n__a =
n__a
n__e =
n__e
n__i =
n__i
n__o =
n__o
n__u =
n__u
a =
a
e =
e
i =
i
o =
o
u =
u
Recursive path order with status [RPO].
Quasi-Precedence:
[2, U713, n2] > U213 > U223 > U233 > U243 > U252 > isList1 > [nil, tt, nnil] > isPalListKind1 > U631
[2, U713, n2] > U213 > U223 > U233 > U243 > U252 > isList1 > [nil, tt, nnil] > U322 > U331 > U631
[2, U713, n2] > U213 > U223 > U233 > U243 > U252 > isList1 > [nil, tt, nnil] > U461 > U631
[2, U713, n2] > U213 > U223 > U233 > U243 > U252 > isList1 > [nil, tt, nnil] > U622 > U631
[2, U713, n2] > U213 > U223 > U233 > U243 > U252 > isList1 > U112 > [U122, isNeList1, U452] > U312 > isPalListKind1 > U631
[2, U713, n2] > U213 > U223 > U233 > U243 > U252 > isList1 > U112 > [U122, isNeList1, U452] > U312 > U322 > U331 > U631
[2, U713, n2] > U213 > U223 > U233 > U243 > U252 > isList1 > U112 > [U122, isNeList1, U452] > U461 > U631
[2, U713, n2] > U413 > U423 > U433 > U443 > isList1 > [nil, tt, nnil] > isPalListKind1 > U631
[2, U713, n2] > U413 > U423 > U433 > U443 > isList1 > [nil, tt, nnil] > U322 > U331 > U631
[2, U713, n2] > U413 > U423 > U433 > U443 > isList1 > [nil, tt, nnil] > U461 > U631
[2, U713, n2] > U413 > U423 > U433 > U443 > isList1 > [nil, tt, nnil] > U622 > U631
[2, U713, n2] > U413 > U423 > U433 > U443 > isList1 > U112 > [U122, isNeList1, U452] > U312 > isPalListKind1 > U631
[2, U713, n2] > U413 > U423 > U433 > U443 > isList1 > U112 > [U122, isNeList1, U452] > U312 > U322 > U331 > U631
[2, U713, n2] > U413 > U423 > U433 > U443 > isList1 > U112 > [U122, isNeList1, U452] > U461 > U631
[2, U713, n2] > U513 > U523 > U533 > U543 > U552 > isList1 > [nil, tt, nnil] > isPalListKind1 > U631
[2, U713, n2] > U513 > U523 > U533 > U543 > U552 > isList1 > [nil, tt, nnil] > U322 > U331 > U631
[2, U713, n2] > U513 > U523 > U533 > U543 > U552 > isList1 > [nil, tt, nnil] > U461 > U631
[2, U713, n2] > U513 > U523 > U533 > U543 > U552 > isList1 > [nil, tt, nnil] > U622 > U631
[2, U713, n2] > U513 > U523 > U533 > U543 > U552 > isList1 > U112 > [U122, isNeList1, U452] > U312 > isPalListKind1 > U631
[2, U713, n2] > U513 > U523 > U533 > U543 > U552 > isList1 > U112 > [U122, isNeList1, U452] > U312 > U322 > U331 > U631
[2, U713, n2] > U513 > U523 > U533 > U543 > U552 > isList1 > U112 > [U122, isNeList1, U452] > U461 > U631
[2, U713, n2] > U722 > U732 > U741 > [nil, tt, nnil] > isPalListKind1 > U631
[2, U713, n2] > U722 > U732 > U741 > [nil, tt, nnil] > U322 > U331 > U631
[2, U713, n2] > U722 > U732 > U741 > [nil, tt, nnil] > U461 > U631
[2, U713, n2] > U722 > U732 > U741 > [nil, tt, nnil] > U622 > U631
[2, U713, n2] > U722 > isPal1 > [nil, tt, nnil] > isPalListKind1 > U631
[2, U713, n2] > U722 > isPal1 > [nil, tt, nnil] > U322 > U331 > U631
[2, U713, n2] > U722 > isPal1 > [nil, tt, nnil] > U461 > U631
[2, U713, n2] > U722 > isPal1 > [nil, tt, nnil] > U622 > U631
[2, U713, n2] > U722 > isPal1 > U812 > U822 > isNePal1 > U612 > isPalListKind1 > U631
[2, U713, n2] > U722 > isPal1 > U812 > U822 > isNePal1 > U612 > U622 > U631
[2, U713, n2] > U912 > isPalListKind1 > U631
[na, a] > [nil, tt, nnil] > isPalListKind1 > U631
[na, a] > [nil, tt, nnil] > U322 > U331 > U631
[na, a] > [nil, tt, nnil] > U461 > U631
[na, a] > [nil, tt, nnil] > U622 > U631
[ne, e] > [nil, tt, nnil] > isPalListKind1 > U631
[ne, e] > [nil, tt, nnil] > U322 > U331 > U631
[ne, e] > [nil, tt, nnil] > U461 > U631
[ne, e] > [nil, tt, nnil] > U622 > U631
[ni, i] > [nil, tt, nnil] > isPalListKind1 > U631
[ni, i] > [nil, tt, nnil] > U322 > U331 > U631
[ni, i] > [nil, tt, nnil] > U461 > U631
[ni, i] > [nil, tt, nnil] > U622 > U631
[no, o] > [nil, tt, nnil] > isPalListKind1 > U631
[no, o] > [nil, tt, nnil] > U322 > U331 > U631
[no, o] > [nil, tt, nnil] > U461 > U631
[no, o] > [nil, tt, nnil] > U622 > U631
[nu, u] > [nil, tt, nnil] > isPalListKind1 > U631
[nu, u] > [nil, tt, nnil] > U322 > U331 > U631
[nu, u] > [nil, tt, nnil] > U461 > U631
[nu, u] > [nil, tt, nnil] > U622 > U631
Status:
i: multiset
U622: [1,2]
U413: multiset
U322: [1,2]
U252: multiset
ni: multiset
U243: multiset
U122: multiset
nnil: multiset
tt: multiset
U223: multiset
isPalListKind1: multiset
U213: multiset
U543: multiset
nil: multiset
U552: [1,2]
U312: multiset
e: multiset
isNePal1: multiset
n2: [1,2]
o: multiset
U533: multiset
no: multiset
U233: multiset
U812: [2,1]
U443: multiset
U331: [1]
U741: [1]
U713: [1,3,2]
U912: multiset
nu: multiset
_2: [1,2]
U433: multiset
na: multiset
U423: multiset
U452: multiset
U513: multiset
U732: multiset
a: multiset
isList1: multiset
ne: multiset
U722: multiset
U112: multiset
U631: multiset
U523: multiset
isPal1: multiset
U822: [1,2]
U612: multiset
u: multiset
U461: [1]
isNeList1: multiset
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(activate(V)), activate(V))
U12(tt, V) → U13(isNeList(activate(V)))
U21(tt, V1, V2) → U22(isPalListKind(activate(V1)), activate(V1), activate(V2))
U22(tt, V1, V2) → U23(isPalListKind(activate(V2)), activate(V1), activate(V2))
U23(tt, V1, V2) → U24(isPalListKind(activate(V2)), activate(V1), activate(V2))
U24(tt, V1, V2) → U25(isList(activate(V1)), activate(V2))
U25(tt, V2) → U26(isList(activate(V2)))
U31(tt, V) → U32(isPalListKind(activate(V)), activate(V))
U32(tt, V) → U33(isQid(activate(V)))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isPalListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isPalListKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isList(activate(V1)), activate(V2))
U45(tt, V2) → U46(isNeList(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isPalListKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isPalListKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNeList(activate(V1)), activate(V2))
U55(tt, V2) → U56(isList(activate(V2)))
U61(tt, V) → U62(isPalListKind(activate(V)), activate(V))
U62(tt, V) → U63(isQid(activate(V)))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(activate(I)), activate(P))
U72(tt, P) → U73(isPal(activate(P)), activate(P))
U73(tt, P) → U74(isPalListKind(activate(P)))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(activate(V)), activate(V))
U82(tt, V) → U83(isNePal(activate(V)))
U91(tt, V2) → U92(isPalListKind(activate(V2)))
isList(V) → U11(isPalListKind(activate(V)), activate(V))
isList(n__nil) → tt
isList(n____(V1, V2)) → U21(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(V) → U31(isPalListKind(activate(V)), activate(V))
isNeList(n____(V1, V2)) → U41(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNeList(n____(V1, V2)) → U51(isPalListKind(activate(V1)), activate(V1), activate(V2))
isNePal(V) → U61(isPalListKind(activate(V)), activate(V))
isNePal(n____(I, n____(P, I))) → U71(isQid(activate(I)), activate(I), activate(P))
isPal(V) → U81(isPalListKind(activate(V)), activate(V))
isPal(n__nil) → tt
isPalListKind(n__a) → tt
isPalListKind(n__e) → tt
isPalListKind(n__i) → tt
isPalListKind(n__nil) → tt
isPalListKind(n__o) → tt
isPalListKind(n__u) → tt
isPalListKind(n____(V1, V2)) → U91(isPalListKind(activate(V1)), activate(V2))
isQid(n__a) → tt
isQid(n__e) → tt
isQid(n__i) → tt
isQid(n__o) → tt
isQid(n__u) → tt
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
U13(tt) → tt
U26(tt) → tt
U56(tt) → tt
U83(tt) → tt
U92(tt) → tt
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X
Q is empty.
(3) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(U13(x1)) = 1 + x1
POL(U26(x1)) = 1 + x1
POL(U56(x1)) = 1 + x1
POL(U83(x1)) = 1 + x1
POL(U92(x1)) = 1 + x1
POL(__(x1, x2)) = x1 + x2
POL(a) = 0
POL(activate(x1)) = x1
POL(e) = 0
POL(i) = 0
POL(n____(x1, x2)) = x1 + x2
POL(n__a) = 0
POL(n__e) = 0
POL(n__i) = 0
POL(n__nil) = 0
POL(n__o) = 0
POL(n__u) = 0
POL(nil) = 0
POL(o) = 0
POL(tt) = 0
POL(u) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
U13(tt) → tt
U26(tt) → tt
U56(tt) → tt
U83(tt) → tt
U92(tt) → tt
(4) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
nil → n__nil
__(X1, X2) → n____(X1, X2)
a → n__a
e → n__e
i → n__i
o → n__o
u → n__u
activate(n__nil) → nil
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__o) → o
activate(n__u) → u
activate(X) → X
Q is empty.
(5) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(__(x1, x2)) = 2 + 2·x1 + x2
POL(a) = 2
POL(activate(x1)) = 1 + 2·x1
POL(e) = 2
POL(i) = 1
POL(n____(x1, x2)) = 2 + 2·x1 + x2
POL(n__a) = 2
POL(n__e) = 1
POL(n__i) = 1
POL(n__nil) = 1
POL(n__o) = 0
POL(n__u) = 2
POL(nil) = 2
POL(o) = 1
POL(u) = 2
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
nil → n__nil
e → n__e
o → n__o
activate(n__nil) → nil
activate(n__a) → a
activate(n__e) → e
activate(n__i) → i
activate(n__u) → u
activate(X) → X
(6) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
__(X1, X2) → n____(X1, X2)
a → n__a
i → n__i
u → n__u
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
activate(n__o) → o
Q is empty.
(7) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(__(x1, x2)) = x1 + x2
POL(a) = 1
POL(activate(x1)) = x1
POL(i) = 1
POL(n____(x1, x2)) = x1 + x2
POL(n__a) = 0
POL(n__i) = 0
POL(n__o) = 1
POL(n__u) = 0
POL(o) = 0
POL(u) = 1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
a → n__a
i → n__i
u → n__u
activate(n__o) → o
(8) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
__(X1, X2) → n____(X1, X2)
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
Q is empty.
(9) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(__(x1, x2)) = 1 + 2·x1 + 2·x2
POL(activate(x1)) = 2·x1
POL(n____(x1, x2)) = 1 + 2·x1 + 2·x2
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
activate(n____(X1, X2)) → __(activate(X1), activate(X2))
(10) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
__(X1, X2) → n____(X1, X2)
Q is empty.
(11) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(__(x1, x2)) = 2 + 2·x1 + 2·x2
POL(n____(x1, x2)) = 1 + x1 + x2
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
__(X1, X2) → n____(X1, X2)
(12) Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.
(13) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(14) TRUE
(15) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(16) TRUE
(17) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(18) TRUE