Problem:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil()) -> X
__(nil(),X) -> X
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U72(tt()) -> tt()
U81(tt()) -> tt()
isList(V) -> U11(isNeList(activate(V)))
isList(n__nil()) -> tt()
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isNeList(V) -> U31(isQid(activate(V)))
isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isPal(V) -> U81(isNePal(activate(V)))
isPal(n__nil()) -> tt()
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)) -> __(X1,X2)
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__o()) -> o()
activate(n__u()) -> u()
activate(X) -> X
Proof:
Complexity Transformation Processor:
strict:
__(__(X,Y),Z) -> __(X,__(Y,Z))
__(X,nil()) -> X
__(nil(),X) -> X
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U71(tt(),P) -> U72(isPal(activate(P)))
U72(tt()) -> tt()
U81(tt()) -> tt()
isList(V) -> U11(isNeList(activate(V)))
isList(n__nil()) -> tt()
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isNeList(V) -> U31(isQid(activate(V)))
isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isPal(V) -> U81(isNePal(activate(V)))
isPal(n__nil()) -> tt()
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)) -> __(X1,X2)
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__o()) -> o()
activate(n__u()) -> u()
activate(X) -> X
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[u] = 0,
[o] = 0,
[i] = 0,
[e] = 0,
[a] = 0,
[n__u] = 0,
[n__o] = 0,
[n__i] = 8,
[n__e] = 3,
[n__a] = 0,
[isNePal](x0) = x0 + 10,
[isQid](x0) = x0 + 13,
[n____](x0, x1) = x0 + x1,
[n__nil] = 8,
[U81](x0) = x0 + 12,
[U72](x0) = x0 + 12,
[isPal](x0) = x0 + 2,
[U71](x0, x1) = x0 + x1 + 6,
[U61](x0) = x0 + 7,
[U52](x0) = x0 + 4,
[U51](x0, x1) = x0 + x1 + 9,
[U42](x0) = x0 + 4,
[isNeList](x0) = x0 + 10,
[U41](x0, x1) = x0 + x1 + 7,
[U31](x0) = x0 + 6,
[U22](x0) = x0 + 2,
[isList](x0) = x0 + 5,
[activate](x0) = x0 + 5,
[U21](x0, x1) = x0 + x1 + 6,
[U11](x0) = x0 + 8,
[tt] = 8,
[nil] = 4,
[__](x0, x1) = x0 + x1 + 10
orientation:
__(__(X,Y),Z) = X + Y + Z + 20 >= X + Y + Z + 20 = __(X,__(Y,Z))
__(X,nil()) = X + 14 >= X = X
__(nil(),X) = X + 14 >= X = X
U11(tt()) = 16 >= 8 = tt()
U21(tt(),V2) = V2 + 14 >= V2 + 12 = U22(isList(activate(V2)))
U22(tt()) = 10 >= 8 = tt()
U31(tt()) = 14 >= 8 = tt()
U41(tt(),V2) = V2 + 15 >= V2 + 19 = U42(isNeList(activate(V2)))
U42(tt()) = 12 >= 8 = tt()
U51(tt(),V2) = V2 + 17 >= V2 + 14 = U52(isList(activate(V2)))
U52(tt()) = 12 >= 8 = tt()
U61(tt()) = 15 >= 8 = tt()
U71(tt(),P) = P + 14 >= P + 19 = U72(isPal(activate(P)))
U72(tt()) = 20 >= 8 = tt()
U81(tt()) = 20 >= 8 = tt()
isList(V) = V + 5 >= V + 23 = U11(isNeList(activate(V)))
isList(n__nil()) = 13 >= 8 = tt()
isList(n____(V1,V2)) = V1 + V2 + 5 >= V1 + V2 + 21 = U21(isList(activate(V1)),activate(V2))
isNeList(V) = V + 10 >= V + 24 = U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 22 = U41(isList(activate(V1)),activate(V2))
isNeList(n____(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 29 = U51(isNeList(activate(V1)),activate(V2))
isNePal(V) = V + 10 >= V + 25 = U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) = 2I + P + 20 >= I + P + 29 = U71(isQid(activate(I)),activate(P))
isPal(V) = V + 2 >= V + 27 = U81(isNePal(activate(V)))
isPal(n__nil()) = 10 >= 8 = tt()
isQid(n__a()) = 13 >= 8 = tt()
isQid(n__e()) = 16 >= 8 = tt()
isQid(n__i()) = 21 >= 8 = tt()
isQid(n__o()) = 13 >= 8 = tt()
isQid(n__u()) = 13 >= 8 = tt()
nil() = 4 >= 8 = n__nil()
__(X1,X2) = X1 + X2 + 10 >= X1 + X2 = n____(X1,X2)
a() = 0 >= 0 = n__a()
e() = 0 >= 3 = n__e()
i() = 0 >= 8 = n__i()
o() = 0 >= 0 = n__o()
u() = 0 >= 0 = n__u()
activate(n__nil()) = 13 >= 4 = nil()
activate(n____(X1,X2)) = X1 + X2 + 5 >= X1 + X2 + 10 = __(X1,X2)
activate(n__a()) = 5 >= 0 = a()
activate(n__e()) = 8 >= 0 = e()
activate(n__i()) = 13 >= 0 = i()
activate(n__o()) = 5 >= 0 = o()
activate(n__u()) = 5 >= 0 = u()
activate(X) = X + 5 >= X = X
problem:
strict:
__(__(X,Y),Z) -> __(X,__(Y,Z))
U41(tt(),V2) -> U42(isNeList(activate(V2)))
U71(tt(),P) -> U72(isPal(activate(P)))
isList(V) -> U11(isNeList(activate(V)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isNeList(V) -> U31(isQid(activate(V)))
isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isPal(V) -> U81(isNePal(activate(V)))
nil() -> n__nil()
a() -> n__a()
e() -> n__e()
i() -> n__i()
o() -> n__o()
u() -> n__u()
activate(n____(X1,X2)) -> __(X1,X2)
weak:
__(X,nil()) -> X
__(nil(),X) -> X
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U72(tt()) -> tt()
U81(tt()) -> tt()
isList(n__nil()) -> tt()
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> tt()
__(X1,X2) -> n____(X1,X2)
activate(n__nil()) -> nil()
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__o()) -> o()
activate(n__u()) -> u()
activate(X) -> X
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[u] = 10,
[o] = 10,
[i] = 10,
[e] = 10,
[a] = 10,
[n__u] = 2,
[n__o] = 2,
[n__i] = 2,
[n__e] = 2,
[n__a] = 2,
[isNePal](x0) = x0 + 1,
[isQid](x0) = x0 + 5,
[n____](x0, x1) = x0 + x1 + 12,
[n__nil] = 5,
[U81](x0) = x0,
[U72](x0) = x0,
[isPal](x0) = x0 + 2,
[U71](x0, x1) = x0 + x1 + 10,
[U61](x0) = x0,
[U52](x0) = x0,
[U51](x0, x1) = x0 + x1 + 3,
[U42](x0) = x0,
[isNeList](x0) = x0 + 9,
[U41](x0, x1) = x0 + x1,
[U31](x0) = x0,
[U22](x0) = x0,
[isList](x0) = x0 + 2,
[activate](x0) = x0 + 8,
[U21](x0, x1) = x0 + x1 + 3,
[U11](x0) = x0,
[tt] = 7,
[nil] = 13,
[__](x0, x1) = x0 + x1 + 14
orientation:
__(__(X,Y),Z) = X + Y + Z + 28 >= X + Y + Z + 28 = __(X,__(Y,Z))
U41(tt(),V2) = V2 + 7 >= V2 + 17 = U42(isNeList(activate(V2)))
U71(tt(),P) = P + 17 >= P + 10 = U72(isPal(activate(P)))
isList(V) = V + 2 >= V + 17 = U11(isNeList(activate(V)))
isList(n____(V1,V2)) = V1 + V2 + 14 >= V1 + V2 + 21 = U21(isList(activate(V1)),activate(V2))
isNeList(V) = V + 9 >= V + 13 = U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = V1 + V2 + 21 >= V1 + V2 + 18 = U41(isList(activate(V1)),activate(V2))
isNeList(n____(V1,V2)) = V1 + V2 + 21 >= V1 + V2 + 28 = U51(isNeList(activate(V1)),activate(V2))
isNePal(V) = V + 1 >= V + 13 = U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) = 2I + P + 27 >= I + P + 31 = U71(isQid(activate(I)),activate(P))
isPal(V) = V + 2 >= V + 9 = U81(isNePal(activate(V)))
nil() = 13 >= 5 = n__nil()
a() = 10 >= 2 = n__a()
e() = 10 >= 2 = n__e()
i() = 10 >= 2 = n__i()
o() = 10 >= 2 = n__o()
u() = 10 >= 2 = n__u()
activate(n____(X1,X2)) = X1 + X2 + 20 >= X1 + X2 + 14 = __(X1,X2)
__(X,nil()) = X + 27 >= X = X
__(nil(),X) = X + 27 >= X = X
U11(tt()) = 7 >= 7 = tt()
U21(tt(),V2) = V2 + 10 >= V2 + 10 = U22(isList(activate(V2)))
U22(tt()) = 7 >= 7 = tt()
U31(tt()) = 7 >= 7 = tt()
U42(tt()) = 7 >= 7 = tt()
U51(tt(),V2) = V2 + 10 >= V2 + 10 = U52(isList(activate(V2)))
U52(tt()) = 7 >= 7 = tt()
U61(tt()) = 7 >= 7 = tt()
U72(tt()) = 7 >= 7 = tt()
U81(tt()) = 7 >= 7 = tt()
isList(n__nil()) = 7 >= 7 = tt()
isPal(n__nil()) = 7 >= 7 = tt()
isQid(n__a()) = 7 >= 7 = tt()
isQid(n__e()) = 7 >= 7 = tt()
isQid(n__i()) = 7 >= 7 = tt()
isQid(n__o()) = 7 >= 7 = tt()
isQid(n__u()) = 7 >= 7 = tt()
__(X1,X2) = X1 + X2 + 14 >= X1 + X2 + 12 = n____(X1,X2)
activate(n__nil()) = 13 >= 13 = nil()
activate(n__a()) = 10 >= 10 = a()
activate(n__e()) = 10 >= 10 = e()
activate(n__i()) = 10 >= 10 = i()
activate(n__o()) = 10 >= 10 = o()
activate(n__u()) = 10 >= 10 = u()
activate(X) = X + 8 >= X = X
problem:
strict:
__(__(X,Y),Z) -> __(X,__(Y,Z))
U41(tt(),V2) -> U42(isNeList(activate(V2)))
isList(V) -> U11(isNeList(activate(V)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isNeList(V) -> U31(isQid(activate(V)))
isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
isNePal(V) -> U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isPal(V) -> U81(isNePal(activate(V)))
weak:
U71(tt(),P) -> U72(isPal(activate(P)))
isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
nil() -> n__nil()
a() -> n__a()
e() -> n__e()
i() -> n__i()
o() -> n__o()
u() -> n__u()
activate(n____(X1,X2)) -> __(X1,X2)
__(X,nil()) -> X
__(nil(),X) -> X
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U72(tt()) -> tt()
U81(tt()) -> tt()
isList(n__nil()) -> tt()
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> tt()
__(X1,X2) -> n____(X1,X2)
activate(n__nil()) -> nil()
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__o()) -> o()
activate(n__u()) -> u()
activate(X) -> X
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[u] = 0,
[o] = 3,
[i] = 14,
[e] = 8,
[a] = 0,
[n__u] = 0,
[n__o] = 3,
[n__i] = 14,
[n__e] = 8,
[n__a] = 0,
[isNePal](x0) = x0 + 14,
[isQid](x0) = x0 + 3,
[n____](x0, x1) = x0 + x1,
[n__nil] = 0,
[U81](x0) = x0,
[U72](x0) = x0,
[isPal](x0) = x0 + 15,
[U71](x0, x1) = x0 + x1 + 13,
[U61](x0) = x0 + 9,
[U52](x0) = x0,
[U51](x0, x1) = x0 + x1 + 14,
[U42](x0) = x0,
[isNeList](x0) = x0 + 12,
[U41](x0, x1) = x0 + x1,
[U31](x0) = x0 + 12,
[U22](x0) = x0 + 1,
[isList](x0) = x0 + 12,
[activate](x0) = x0,
[U21](x0, x1) = x0 + x1 + 12,
[U11](x0) = x0 + 14,
[tt] = 2,
[nil] = 0,
[__](x0, x1) = x0 + x1
orientation:
__(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))
U41(tt(),V2) = V2 + 2 >= V2 + 12 = U42(isNeList(activate(V2)))
isList(V) = V + 12 >= V + 26 = U11(isNeList(activate(V)))
isList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 24 = U21(isList(activate(V1)),activate(V2))
isNeList(V) = V + 12 >= V + 15 = U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 26 = U51(isNeList(activate(V1)),activate(V2))
isNePal(V) = V + 14 >= V + 12 = U61(isQid(activate(V)))
isNePal(n____(I,__(P,I))) = 2I + P + 14 >= I + P + 16 = U71(isQid(activate(I)),activate(P))
isPal(V) = V + 15 >= V + 14 = U81(isNePal(activate(V)))
U71(tt(),P) = P + 15 >= P + 15 = U72(isPal(activate(P)))
isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = U41(isList(activate(V1)),activate(V2))
nil() = 0 >= 0 = n__nil()
a() = 0 >= 0 = n__a()
e() = 8 >= 8 = n__e()
i() = 14 >= 14 = n__i()
o() = 3 >= 3 = n__o()
u() = 0 >= 0 = n__u()
activate(n____(X1,X2)) = X1 + X2 >= X1 + X2 = __(X1,X2)
__(X,nil()) = X >= X = X
__(nil(),X) = X >= X = X
U11(tt()) = 16 >= 2 = tt()
U21(tt(),V2) = V2 + 14 >= V2 + 13 = U22(isList(activate(V2)))
U22(tt()) = 3 >= 2 = tt()
U31(tt()) = 14 >= 2 = tt()
U42(tt()) = 2 >= 2 = tt()
U51(tt(),V2) = V2 + 16 >= V2 + 12 = U52(isList(activate(V2)))
U52(tt()) = 2 >= 2 = tt()
U61(tt()) = 11 >= 2 = tt()
U72(tt()) = 2 >= 2 = tt()
U81(tt()) = 2 >= 2 = tt()
isList(n__nil()) = 12 >= 2 = tt()
isPal(n__nil()) = 15 >= 2 = tt()
isQid(n__a()) = 3 >= 2 = tt()
isQid(n__e()) = 11 >= 2 = tt()
isQid(n__i()) = 17 >= 2 = tt()
isQid(n__o()) = 6 >= 2 = tt()
isQid(n__u()) = 3 >= 2 = tt()
__(X1,X2) = X1 + X2 >= X1 + X2 = n____(X1,X2)
activate(n__nil()) = 0 >= 0 = nil()
activate(n__a()) = 0 >= 0 = a()
activate(n__e()) = 8 >= 8 = e()
activate(n__i()) = 14 >= 14 = i()
activate(n__o()) = 3 >= 3 = o()
activate(n__u()) = 0 >= 0 = u()
activate(X) = X >= X = X
problem:
strict:
__(__(X,Y),Z) -> __(X,__(Y,Z))
U41(tt(),V2) -> U42(isNeList(activate(V2)))
isList(V) -> U11(isNeList(activate(V)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isNeList(V) -> U31(isQid(activate(V)))
isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
weak:
isNePal(V) -> U61(isQid(activate(V)))
isPal(V) -> U81(isNePal(activate(V)))
U71(tt(),P) -> U72(isPal(activate(P)))
isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
nil() -> n__nil()
a() -> n__a()
e() -> n__e()
i() -> n__i()
o() -> n__o()
u() -> n__u()
activate(n____(X1,X2)) -> __(X1,X2)
__(X,nil()) -> X
__(nil(),X) -> X
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U72(tt()) -> tt()
U81(tt()) -> tt()
isList(n__nil()) -> tt()
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> tt()
__(X1,X2) -> n____(X1,X2)
activate(n__nil()) -> nil()
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__o()) -> o()
activate(n__u()) -> u()
activate(X) -> X
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[u] = 2,
[o] = 9,
[i] = 2,
[e] = 4,
[a] = 8,
[n__u] = 2,
[n__o] = 9,
[n__i] = 2,
[n__e] = 4,
[n__a] = 8,
[isNePal](x0) = x0,
[isQid](x0) = x0,
[n____](x0, x1) = x0 + x1,
[n__nil] = 0,
[U81](x0) = x0 + 4,
[U72](x0) = x0 + 3,
[isPal](x0) = x0 + 4,
[U71](x0, x1) = x0 + x1 + 6,
[U61](x0) = x0,
[U52](x0) = x0,
[U51](x0, x1) = x0 + x1 + 11,
[U42](x0) = x0 + 3,
[isNeList](x0) = x0 + 12,
[U41](x0, x1) = x0 + x1,
[U31](x0) = x0 + 5,
[U22](x0) = x0 + 4,
[isList](x0) = x0 + 12,
[activate](x0) = x0,
[U21](x0, x1) = x0 + x1 + 15,
[U11](x0) = x0 + 5,
[tt] = 1,
[nil] = 0,
[__](x0, x1) = x0 + x1
orientation:
__(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))
U41(tt(),V2) = V2 + 1 >= V2 + 15 = U42(isNeList(activate(V2)))
isList(V) = V + 12 >= V + 17 = U11(isNeList(activate(V)))
isList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 27 = U21(isList(activate(V1)),activate(V2))
isNeList(V) = V + 12 >= V + 5 = U31(isQid(activate(V)))
isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 23 = U51(isNeList(activate(V1)),activate(V2))
isNePal(n____(I,__(P,I))) = 2I + P >= I + P + 6 = U71(isQid(activate(I)),activate(P))
isNePal(V) = V >= V = U61(isQid(activate(V)))
isPal(V) = V + 4 >= V + 4 = U81(isNePal(activate(V)))
U71(tt(),P) = P + 7 >= P + 7 = U72(isPal(activate(P)))
isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = U41(isList(activate(V1)),activate(V2))
nil() = 0 >= 0 = n__nil()
a() = 8 >= 8 = n__a()
e() = 4 >= 4 = n__e()
i() = 2 >= 2 = n__i()
o() = 9 >= 9 = n__o()
u() = 2 >= 2 = n__u()
activate(n____(X1,X2)) = X1 + X2 >= X1 + X2 = __(X1,X2)
__(X,nil()) = X >= X = X
__(nil(),X) = X >= X = X
U11(tt()) = 6 >= 1 = tt()
U21(tt(),V2) = V2 + 16 >= V2 + 16 = U22(isList(activate(V2)))
U22(tt()) = 5 >= 1 = tt()
U31(tt()) = 6 >= 1 = tt()
U42(tt()) = 4 >= 1 = tt()
U51(tt(),V2) = V2 + 12 >= V2 + 12 = U52(isList(activate(V2)))
U52(tt()) = 1 >= 1 = tt()
U61(tt()) = 1 >= 1 = tt()
U72(tt()) = 4 >= 1 = tt()
U81(tt()) = 5 >= 1 = tt()
isList(n__nil()) = 12 >= 1 = tt()
isPal(n__nil()) = 4 >= 1 = tt()
isQid(n__a()) = 8 >= 1 = tt()
isQid(n__e()) = 4 >= 1 = tt()
isQid(n__i()) = 2 >= 1 = tt()
isQid(n__o()) = 9 >= 1 = tt()
isQid(n__u()) = 2 >= 1 = tt()
__(X1,X2) = X1 + X2 >= X1 + X2 = n____(X1,X2)
activate(n__nil()) = 0 >= 0 = nil()
activate(n__a()) = 8 >= 8 = a()
activate(n__e()) = 4 >= 4 = e()
activate(n__i()) = 2 >= 2 = i()
activate(n__o()) = 9 >= 9 = o()
activate(n__u()) = 2 >= 2 = u()
activate(X) = X >= X = X
problem:
strict:
__(__(X,Y),Z) -> __(X,__(Y,Z))
U41(tt(),V2) -> U42(isNeList(activate(V2)))
isList(V) -> U11(isNeList(activate(V)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
weak:
isNeList(V) -> U31(isQid(activate(V)))
isNePal(V) -> U61(isQid(activate(V)))
isPal(V) -> U81(isNePal(activate(V)))
U71(tt(),P) -> U72(isPal(activate(P)))
isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
nil() -> n__nil()
a() -> n__a()
e() -> n__e()
i() -> n__i()
o() -> n__o()
u() -> n__u()
activate(n____(X1,X2)) -> __(X1,X2)
__(X,nil()) -> X
__(nil(),X) -> X
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U72(tt()) -> tt()
U81(tt()) -> tt()
isList(n__nil()) -> tt()
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> tt()
__(X1,X2) -> n____(X1,X2)
activate(n__nil()) -> nil()
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__o()) -> o()
activate(n__u()) -> u()
activate(X) -> X
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[u] = 0,
[o] = 0,
[i] = 0,
[e] = 3,
[a] = 0,
[n__u] = 0,
[n__o] = 0,
[n__i] = 0,
[n__e] = 3,
[n__a] = 0,
[isNePal](x0) = x0 + 2,
[isQid](x0) = x0 + 1,
[n____](x0, x1) = x0 + x1 + 7,
[n__nil] = 0,
[U81](x0) = x0 + 5,
[U72](x0) = x0,
[isPal](x0) = x0 + 7,
[U71](x0, x1) = x0 + x1 + 7,
[U61](x0) = x0,
[U52](x0) = x0 + 8,
[U51](x0, x1) = x0 + x1 + 12,
[U42](x0) = x0 + 1,
[isNeList](x0) = x0 + 4,
[U41](x0, x1) = x0 + x1 + 2,
[U31](x0) = x0 + 2,
[U22](x0) = x0 + 2,
[isList](x0) = x0 + 1,
[activate](x0) = x0,
[U21](x0, x1) = x0 + x1 + 3,
[U11](x0) = x0 + 13,
[tt] = 0,
[nil] = 0,
[__](x0, x1) = x0 + x1 + 7
orientation:
__(__(X,Y),Z) = X + Y + Z + 14 >= X + Y + Z + 14 = __(X,__(Y,Z))
U41(tt(),V2) = V2 + 2 >= V2 + 5 = U42(isNeList(activate(V2)))
isList(V) = V + 1 >= V + 17 = U11(isNeList(activate(V)))
isList(n____(V1,V2)) = V1 + V2 + 8 >= V1 + V2 + 4 = U21(isList(activate(V1)),activate(V2))
isNeList(n____(V1,V2)) = V1 + V2 + 11 >= V1 + V2 + 16 = U51(isNeList(activate(V1)),activate(V2))
isNePal(n____(I,__(P,I))) = 2I + P + 16 >= I + P + 8 = U71(isQid(activate(I)),activate(P))
isNeList(V) = V + 4 >= V + 3 = U31(isQid(activate(V)))
isNePal(V) = V + 2 >= V + 1 = U61(isQid(activate(V)))
isPal(V) = V + 7 >= V + 7 = U81(isNePal(activate(V)))
U71(tt(),P) = P + 7 >= P + 7 = U72(isPal(activate(P)))
isNeList(n____(V1,V2)) = V1 + V2 + 11 >= V1 + V2 + 3 = U41(isList(activate(V1)),activate(V2))
nil() = 0 >= 0 = n__nil()
a() = 0 >= 0 = n__a()
e() = 3 >= 3 = n__e()
i() = 0 >= 0 = n__i()
o() = 0 >= 0 = n__o()
u() = 0 >= 0 = n__u()
activate(n____(X1,X2)) = X1 + X2 + 7 >= X1 + X2 + 7 = __(X1,X2)
__(X,nil()) = X + 7 >= X = X
__(nil(),X) = X + 7 >= X = X
U11(tt()) = 13 >= 0 = tt()
U21(tt(),V2) = V2 + 3 >= V2 + 3 = U22(isList(activate(V2)))
U22(tt()) = 2 >= 0 = tt()
U31(tt()) = 2 >= 0 = tt()
U42(tt()) = 1 >= 0 = tt()
U51(tt(),V2) = V2 + 12 >= V2 + 9 = U52(isList(activate(V2)))
U52(tt()) = 8 >= 0 = tt()
U61(tt()) = 0 >= 0 = tt()
U72(tt()) = 0 >= 0 = tt()
U81(tt()) = 5 >= 0 = tt()
isList(n__nil()) = 1 >= 0 = tt()
isPal(n__nil()) = 7 >= 0 = tt()
isQid(n__a()) = 1 >= 0 = tt()
isQid(n__e()) = 4 >= 0 = tt()
isQid(n__i()) = 1 >= 0 = tt()
isQid(n__o()) = 1 >= 0 = tt()
isQid(n__u()) = 1 >= 0 = tt()
__(X1,X2) = X1 + X2 + 7 >= X1 + X2 + 7 = n____(X1,X2)
activate(n__nil()) = 0 >= 0 = nil()
activate(n__a()) = 0 >= 0 = a()
activate(n__e()) = 3 >= 3 = e()
activate(n__i()) = 0 >= 0 = i()
activate(n__o()) = 0 >= 0 = o()
activate(n__u()) = 0 >= 0 = u()
activate(X) = X >= X = X
problem:
strict:
__(__(X,Y),Z) -> __(X,__(Y,Z))
U41(tt(),V2) -> U42(isNeList(activate(V2)))
isList(V) -> U11(isNeList(activate(V)))
isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
weak:
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isNeList(V) -> U31(isQid(activate(V)))
isNePal(V) -> U61(isQid(activate(V)))
isPal(V) -> U81(isNePal(activate(V)))
U71(tt(),P) -> U72(isPal(activate(P)))
isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
nil() -> n__nil()
a() -> n__a()
e() -> n__e()
i() -> n__i()
o() -> n__o()
u() -> n__u()
activate(n____(X1,X2)) -> __(X1,X2)
__(X,nil()) -> X
__(nil(),X) -> X
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U72(tt()) -> tt()
U81(tt()) -> tt()
isList(n__nil()) -> tt()
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> tt()
__(X1,X2) -> n____(X1,X2)
activate(n__nil()) -> nil()
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__o()) -> o()
activate(n__u()) -> u()
activate(X) -> X
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[u] = 9,
[o] = 13,
[i] = 13,
[e] = 14,
[a] = 12,
[n__u] = 9,
[n__o] = 12,
[n__i] = 12,
[n__e] = 14,
[n__a] = 12,
[isNePal](x0) = x0 + 9,
[isQid](x0) = x0,
[n____](x0, x1) = x0 + x1 + 2,
[n__nil] = 8,
[U81](x0) = x0 + 1,
[U72](x0) = x0 + 1,
[isPal](x0) = x0 + 15,
[U71](x0, x1) = x0 + x1 + 8,
[U61](x0) = x0 + 2,
[U52](x0) = x0 + 9,
[U51](x0, x1) = x0 + x1 + 7,
[U42](x0) = x0,
[isNeList](x0) = x0 + 15,
[U41](x0, x1) = x0 + x1 + 8,
[U31](x0) = x0 + 1,
[U22](x0) = x0 + 2,
[isList](x0) = x0 + 1,
[activate](x0) = x0 + 1,
[U21](x0, x1) = x0 + x1,
[U11](x0) = x0 + 4,
[tt] = 9,
[nil] = 8,
[__](x0, x1) = x0 + x1 + 2
orientation:
__(__(X,Y),Z) = X + Y + Z + 4 >= X + Y + Z + 4 = __(X,__(Y,Z))
U41(tt(),V2) = V2 + 17 >= V2 + 16 = U42(isNeList(activate(V2)))
isList(V) = V + 1 >= V + 20 = U11(isNeList(activate(V)))
isNeList(n____(V1,V2)) = V1 + V2 + 17 >= V1 + V2 + 24 = U51(isNeList(activate(V1)),activate(V2))
isList(n____(V1,V2)) = V1 + V2 + 3 >= V1 + V2 + 3 = U21(isList(activate(V1)),activate(V2))
isNePal(n____(I,__(P,I))) = 2I + P + 13 >= I + P + 10 = U71(isQid(activate(I)),activate(P))
isNeList(V) = V + 15 >= V + 2 = U31(isQid(activate(V)))
isNePal(V) = V + 9 >= V + 3 = U61(isQid(activate(V)))
isPal(V) = V + 15 >= V + 11 = U81(isNePal(activate(V)))
U71(tt(),P) = P + 17 >= P + 17 = U72(isPal(activate(P)))
isNeList(n____(V1,V2)) = V1 + V2 + 17 >= V1 + V2 + 11 = U41(isList(activate(V1)),activate(V2))
nil() = 8 >= 8 = n__nil()
a() = 12 >= 12 = n__a()
e() = 14 >= 14 = n__e()
i() = 13 >= 12 = n__i()
o() = 13 >= 12 = n__o()
u() = 9 >= 9 = n__u()
activate(n____(X1,X2)) = X1 + X2 + 3 >= X1 + X2 + 2 = __(X1,X2)
__(X,nil()) = X + 10 >= X = X
__(nil(),X) = X + 10 >= X = X
U11(tt()) = 13 >= 9 = tt()
U21(tt(),V2) = V2 + 9 >= V2 + 4 = U22(isList(activate(V2)))
U22(tt()) = 11 >= 9 = tt()
U31(tt()) = 10 >= 9 = tt()
U42(tt()) = 9 >= 9 = tt()
U51(tt(),V2) = V2 + 16 >= V2 + 11 = U52(isList(activate(V2)))
U52(tt()) = 18 >= 9 = tt()
U61(tt()) = 11 >= 9 = tt()
U72(tt()) = 10 >= 9 = tt()
U81(tt()) = 10 >= 9 = tt()
isList(n__nil()) = 9 >= 9 = tt()
isPal(n__nil()) = 23 >= 9 = tt()
isQid(n__a()) = 12 >= 9 = tt()
isQid(n__e()) = 14 >= 9 = tt()
isQid(n__i()) = 12 >= 9 = tt()
isQid(n__o()) = 12 >= 9 = tt()
isQid(n__u()) = 9 >= 9 = tt()
__(X1,X2) = X1 + X2 + 2 >= X1 + X2 + 2 = n____(X1,X2)
activate(n__nil()) = 9 >= 8 = nil()
activate(n__a()) = 13 >= 12 = a()
activate(n__e()) = 15 >= 14 = e()
activate(n__i()) = 13 >= 13 = i()
activate(n__o()) = 13 >= 13 = o()
activate(n__u()) = 10 >= 9 = u()
activate(X) = X + 1 >= X = X
problem:
strict:
__(__(X,Y),Z) -> __(X,__(Y,Z))
isList(V) -> U11(isNeList(activate(V)))
isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
weak:
U41(tt(),V2) -> U42(isNeList(activate(V2)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isNeList(V) -> U31(isQid(activate(V)))
isNePal(V) -> U61(isQid(activate(V)))
isPal(V) -> U81(isNePal(activate(V)))
U71(tt(),P) -> U72(isPal(activate(P)))
isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
nil() -> n__nil()
a() -> n__a()
e() -> n__e()
i() -> n__i()
o() -> n__o()
u() -> n__u()
activate(n____(X1,X2)) -> __(X1,X2)
__(X,nil()) -> X
__(nil(),X) -> X
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U72(tt()) -> tt()
U81(tt()) -> tt()
isList(n__nil()) -> tt()
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> tt()
__(X1,X2) -> n____(X1,X2)
activate(n__nil()) -> nil()
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__o()) -> o()
activate(n__u()) -> u()
activate(X) -> X
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[u] = 8,
[o] = 9,
[i] = 9,
[e] = 9,
[a] = 9,
[n__u] = 8,
[n__o] = 9,
[n__i] = 9,
[n__e] = 9,
[n__a] = 9,
[isNePal](x0) = x0,
[isQid](x0) = x0,
[n____](x0, x1) = x0 + x1 + 15,
[n__nil] = 0,
[U81](x0) = x0 + 2,
[U72](x0) = x0 + 13,
[isPal](x0) = x0 + 8,
[U71](x0, x1) = x0 + x1 + 13,
[U61](x0) = x0,
[U52](x0) = x0 + 2,
[U51](x0, x1) = x0 + x1 + 2,
[U42](x0) = x0 + 14,
[isNeList](x0) = x0,
[U41](x0, x1) = x0 + x1 + 7,
[U31](x0) = x0,
[U22](x0) = x0,
[isList](x0) = x0 + 8,
[activate](x0) = x0,
[U21](x0, x1) = x0 + x1,
[U11](x0) = x0 + 7,
[tt] = 8,
[nil] = 0,
[__](x0, x1) = x0 + x1 + 15
orientation:
__(__(X,Y),Z) = X + Y + Z + 30 >= X + Y + Z + 30 = __(X,__(Y,Z))
isList(V) = V + 8 >= V + 7 = U11(isNeList(activate(V)))
isNeList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 2 = U51(isNeList(activate(V1)),activate(V2))
U41(tt(),V2) = V2 + 15 >= V2 + 14 = U42(isNeList(activate(V2)))
isList(n____(V1,V2)) = V1 + V2 + 23 >= V1 + V2 + 8 = U21(isList(activate(V1)),activate(V2))
isNePal(n____(I,__(P,I))) = 2I + P + 30 >= I + P + 13 = U71(isQid(activate(I)),activate(P))
isNeList(V) = V >= V = U31(isQid(activate(V)))
isNePal(V) = V >= V = U61(isQid(activate(V)))
isPal(V) = V + 8 >= V + 2 = U81(isNePal(activate(V)))
U71(tt(),P) = P + 21 >= P + 21 = U72(isPal(activate(P)))
isNeList(n____(V1,V2)) = V1 + V2 + 15 >= V1 + V2 + 15 = U41(isList(activate(V1)),activate(V2))
nil() = 0 >= 0 = n__nil()
a() = 9 >= 9 = n__a()
e() = 9 >= 9 = n__e()
i() = 9 >= 9 = n__i()
o() = 9 >= 9 = n__o()
u() = 8 >= 8 = n__u()
activate(n____(X1,X2)) = X1 + X2 + 15 >= X1 + X2 + 15 = __(X1,X2)
__(X,nil()) = X + 15 >= X = X
__(nil(),X) = X + 15 >= X = X
U11(tt()) = 15 >= 8 = tt()
U21(tt(),V2) = V2 + 8 >= V2 + 8 = U22(isList(activate(V2)))
U22(tt()) = 8 >= 8 = tt()
U31(tt()) = 8 >= 8 = tt()
U42(tt()) = 22 >= 8 = tt()
U51(tt(),V2) = V2 + 10 >= V2 + 10 = U52(isList(activate(V2)))
U52(tt()) = 10 >= 8 = tt()
U61(tt()) = 8 >= 8 = tt()
U72(tt()) = 21 >= 8 = tt()
U81(tt()) = 10 >= 8 = tt()
isList(n__nil()) = 8 >= 8 = tt()
isPal(n__nil()) = 8 >= 8 = tt()
isQid(n__a()) = 9 >= 8 = tt()
isQid(n__e()) = 9 >= 8 = tt()
isQid(n__i()) = 9 >= 8 = tt()
isQid(n__o()) = 9 >= 8 = tt()
isQid(n__u()) = 8 >= 8 = tt()
__(X1,X2) = X1 + X2 + 15 >= X1 + X2 + 15 = n____(X1,X2)
activate(n__nil()) = 0 >= 0 = nil()
activate(n__a()) = 9 >= 9 = a()
activate(n__e()) = 9 >= 9 = e()
activate(n__i()) = 9 >= 9 = i()
activate(n__o()) = 9 >= 9 = o()
activate(n__u()) = 8 >= 8 = u()
activate(X) = X >= X = X
problem:
strict:
__(__(X,Y),Z) -> __(X,__(Y,Z))
weak:
isList(V) -> U11(isNeList(activate(V)))
isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
U41(tt(),V2) -> U42(isNeList(activate(V2)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isNeList(V) -> U31(isQid(activate(V)))
isNePal(V) -> U61(isQid(activate(V)))
isPal(V) -> U81(isNePal(activate(V)))
U71(tt(),P) -> U72(isPal(activate(P)))
isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
nil() -> n__nil()
a() -> n__a()
e() -> n__e()
i() -> n__i()
o() -> n__o()
u() -> n__u()
activate(n____(X1,X2)) -> __(X1,X2)
__(X,nil()) -> X
__(nil(),X) -> X
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U72(tt()) -> tt()
U81(tt()) -> tt()
isList(n__nil()) -> tt()
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> tt()
__(X1,X2) -> n____(X1,X2)
activate(n__nil()) -> nil()
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__o()) -> o()
activate(n__u()) -> u()
activate(X) -> X
Matrix Interpretation Processor:
dimension: 2
max_matrix:
[1 2]
[0 1]
interpretation:
[3]
[u] = [0],
[3]
[o] = [0],
[3]
[i] = [2],
[3]
[e] = [0],
[3]
[a] = [2],
[3]
[n__u] = [0],
[3]
[n__o] = [0],
[3]
[n__i] = [2],
[3]
[n__e] = [0],
[3]
[n__a] = [2],
[1 1] [0]
[isNePal](x0) = [0 0]x0 + [1],
[isQid](x0) = x0,
[1 1] [0]
[n____](x0, x1) = [0 1]x0 + x1 + [1],
[0]
[n__nil] = [2],
[1 1]
[U81](x0) = [0 0]x0,
[1 0]
[U72](x0) = [0 0]x0,
[1 1] [1]
[isPal](x0) = [0 1]x0 + [0],
[1 0] [1 2]
[U71](x0, x1) = [0 0]x0 + [0 0]x1,
[1 1]
[U61](x0) = [0 0]x0,
[1 0]
[U52](x0) = [0 0]x0,
[1 1] [1 0]
[U51](x0, x1) = [0 0]x0 + [0 0]x1,
[1 0]
[U42](x0) = [0 0]x0,
[3]
[isNeList](x0) = x0 + [0],
[1 1] [1 0]
[U41](x0, x1) = [0 1]x0 + [0 0]x1,
[1 0]
[U31](x0) = [0 0]x0,
[1 0]
[U22](x0) = [0 0]x0,
[3]
[isList](x0) = x0 + [0],
[activate](x0) = x0,
[1 1] [1 0] [0]
[U21](x0, x1) = [0 0]x0 + [0 0]x1 + [1],
[1 0]
[U11](x0) = [0 0]x0,
[3]
[tt] = [0],
[0]
[nil] = [2],
[1 1] [0]
[__](x0, x1) = [0 1]x0 + x1 + [1]
orientation:
[1 2] [1 1] [1] [1 1] [1 1] [0]
__(__(X,Y),Z) = [0 1]X + [0 1]Y + Z + [2] >= [0 1]X + [0 1]Y + Z + [2] = __(X,__(Y,Z))
[3] [1 0] [3]
isList(V) = V + [0] >= [0 0]V + [0] = U11(isNeList(activate(V)))
[1 1] [3] [1 1] [1 0] [3]
isNeList(n____(V1,V2)) = [0 1]V1 + V2 + [1] >= [0 0]V1 + [0 0]V2 + [0] = U51(isNeList(activate(V1)),activate(V2))
[1 0] [3] [1 0] [3]
U41(tt(),V2) = [0 0]V2 + [0] >= [0 0]V2 + [0] = U42(isNeList(activate(V2)))
[1 1] [3] [1 1] [1 0] [3]
isList(n____(V1,V2)) = [0 1]V1 + V2 + [1] >= [0 0]V1 + [0 0]V2 + [1] = U21(isList(activate(V1)),activate(V2))
[2 3] [1 2] [2] [1 0] [1 2]
isNePal(n____(I,__(P,I))) = [0 0]I + [0 0]P + [1] >= [0 0]I + [0 0]P = U71(isQid(activate(I)),activate(P))
[3] [1 0]
isNeList(V) = V + [0] >= [0 0]V = U31(isQid(activate(V)))
[1 1] [0] [1 1]
isNePal(V) = [0 0]V + [1] >= [0 0]V = U61(isQid(activate(V)))
[1 1] [1] [1 1] [1]
isPal(V) = [0 1]V + [0] >= [0 0]V + [0] = U81(isNePal(activate(V)))
[1 2] [3] [1 1] [1]
U71(tt(),P) = [0 0]P + [0] >= [0 0]P + [0] = U72(isPal(activate(P)))
[1 1] [3] [1 1] [1 0] [3]
isNeList(n____(V1,V2)) = [0 1]V1 + V2 + [1] >= [0 1]V1 + [0 0]V2 + [0] = U41(isList(activate(V1)),activate(V2))
[0] [0]
nil() = [2] >= [2] = n__nil()
[3] [3]
a() = [2] >= [2] = n__a()
[3] [3]
e() = [0] >= [0] = n__e()
[3] [3]
i() = [2] >= [2] = n__i()
[3] [3]
o() = [0] >= [0] = n__o()
[3] [3]
u() = [0] >= [0] = n__u()
[1 1] [0] [1 1] [0]
activate(n____(X1,X2)) = [0 1]X1 + X2 + [1] >= [0 1]X1 + X2 + [1] = __(X1,X2)
[1 1] [0]
__(X,nil()) = [0 1]X + [3] >= X = X
[2]
__(nil(),X) = X + [3] >= X = X
[3] [3]
U11(tt()) = [0] >= [0] = tt()
[1 0] [3] [1 0] [3]
U21(tt(),V2) = [0 0]V2 + [1] >= [0 0]V2 + [0] = U22(isList(activate(V2)))
[3] [3]
U22(tt()) = [0] >= [0] = tt()
[3] [3]
U31(tt()) = [0] >= [0] = tt()
[3] [3]
U42(tt()) = [0] >= [0] = tt()
[1 0] [3] [1 0] [3]
U51(tt(),V2) = [0 0]V2 + [0] >= [0 0]V2 + [0] = U52(isList(activate(V2)))
[3] [3]
U52(tt()) = [0] >= [0] = tt()
[3] [3]
U61(tt()) = [0] >= [0] = tt()
[3] [3]
U72(tt()) = [0] >= [0] = tt()
[3] [3]
U81(tt()) = [0] >= [0] = tt()
[3] [3]
isList(n__nil()) = [2] >= [0] = tt()
[3] [3]
isPal(n__nil()) = [2] >= [0] = tt()
[3] [3]
isQid(n__a()) = [2] >= [0] = tt()
[3] [3]
isQid(n__e()) = [0] >= [0] = tt()
[3] [3]
isQid(n__i()) = [2] >= [0] = tt()
[3] [3]
isQid(n__o()) = [0] >= [0] = tt()
[3] [3]
isQid(n__u()) = [0] >= [0] = tt()
[1 1] [0] [1 1] [0]
__(X1,X2) = [0 1]X1 + X2 + [1] >= [0 1]X1 + X2 + [1] = n____(X1,X2)
[0] [0]
activate(n__nil()) = [2] >= [2] = nil()
[3] [3]
activate(n__a()) = [2] >= [2] = a()
[3] [3]
activate(n__e()) = [0] >= [0] = e()
[3] [3]
activate(n__i()) = [2] >= [2] = i()
[3] [3]
activate(n__o()) = [0] >= [0] = o()
[3] [3]
activate(n__u()) = [0] >= [0] = u()
activate(X) = X >= X = X
problem:
strict:
weak:
__(__(X,Y),Z) -> __(X,__(Y,Z))
isList(V) -> U11(isNeList(activate(V)))
isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
U41(tt(),V2) -> U42(isNeList(activate(V2)))
isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
isNeList(V) -> U31(isQid(activate(V)))
isNePal(V) -> U61(isQid(activate(V)))
isPal(V) -> U81(isNePal(activate(V)))
U71(tt(),P) -> U72(isPal(activate(P)))
isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
nil() -> n__nil()
a() -> n__a()
e() -> n__e()
i() -> n__i()
o() -> n__o()
u() -> n__u()
activate(n____(X1,X2)) -> __(X1,X2)
__(X,nil()) -> X
__(nil(),X) -> X
U11(tt()) -> tt()
U21(tt(),V2) -> U22(isList(activate(V2)))
U22(tt()) -> tt()
U31(tt()) -> tt()
U42(tt()) -> tt()
U51(tt(),V2) -> U52(isList(activate(V2)))
U52(tt()) -> tt()
U61(tt()) -> tt()
U72(tt()) -> tt()
U81(tt()) -> tt()
isList(n__nil()) -> tt()
isPal(n__nil()) -> tt()
isQid(n__a()) -> tt()
isQid(n__e()) -> tt()
isQid(n__i()) -> tt()
isQid(n__o()) -> tt()
isQid(n__u()) -> tt()
__(X1,X2) -> n____(X1,X2)
activate(n__nil()) -> nil()
activate(n__a()) -> a()
activate(n__e()) -> e()
activate(n__i()) -> i()
activate(n__o()) -> o()
activate(n__u()) -> u()
activate(X) -> X
Qed