a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__and(tt, X) → mark(X)
a__isNePal(__(I, __(P, I))) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNePal(X)) → a__isNePal(mark(X))
mark(nil) → nil
mark(tt) → tt
a____(X1, X2) → __(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNePal(X) → isNePal(X)
↳ QTRS
↳ DependencyPairsProof
a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__and(tt, X) → mark(X)
a__isNePal(__(I, __(P, I))) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNePal(X)) → a__isNePal(mark(X))
mark(nil) → nil
mark(tt) → tt
a____(X1, X2) → __(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNePal(X) → isNePal(X)
A____(__(X, Y), Z) → A____(mark(X), a____(mark(Y), mark(Z)))
MARK(isNePal(X)) → MARK(X)
A____(__(X, Y), Z) → MARK(Z)
A____(__(X, Y), Z) → A____(mark(Y), mark(Z))
MARK(isNePal(X)) → A__ISNEPAL(mark(X))
A__AND(tt, X) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(and(X1, X2)) → A__AND(mark(X1), X2)
A____(__(X, Y), Z) → MARK(X)
MARK(and(X1, X2)) → MARK(X1)
A____(X, nil) → MARK(X)
A____(nil, X) → MARK(X)
MARK(__(X1, X2)) → A____(mark(X1), mark(X2))
A____(__(X, Y), Z) → MARK(Y)
MARK(__(X1, X2)) → MARK(X2)
a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__and(tt, X) → mark(X)
a__isNePal(__(I, __(P, I))) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNePal(X)) → a__isNePal(mark(X))
mark(nil) → nil
mark(tt) → tt
a____(X1, X2) → __(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNePal(X) → isNePal(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
A____(__(X, Y), Z) → A____(mark(X), a____(mark(Y), mark(Z)))
MARK(isNePal(X)) → MARK(X)
A____(__(X, Y), Z) → MARK(Z)
A____(__(X, Y), Z) → A____(mark(Y), mark(Z))
MARK(isNePal(X)) → A__ISNEPAL(mark(X))
A__AND(tt, X) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(and(X1, X2)) → A__AND(mark(X1), X2)
A____(__(X, Y), Z) → MARK(X)
MARK(and(X1, X2)) → MARK(X1)
A____(X, nil) → MARK(X)
A____(nil, X) → MARK(X)
MARK(__(X1, X2)) → A____(mark(X1), mark(X2))
A____(__(X, Y), Z) → MARK(Y)
MARK(__(X1, X2)) → MARK(X2)
a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__and(tt, X) → mark(X)
a__isNePal(__(I, __(P, I))) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNePal(X)) → a__isNePal(mark(X))
mark(nil) → nil
mark(tt) → tt
a____(X1, X2) → __(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNePal(X) → isNePal(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
A____(__(X, Y), Z) → A____(mark(X), a____(mark(Y), mark(Z)))
MARK(isNePal(X)) → MARK(X)
A____(__(X, Y), Z) → MARK(Z)
A____(__(X, Y), Z) → A____(mark(Y), mark(Z))
A__AND(tt, X) → MARK(X)
MARK(__(X1, X2)) → MARK(X1)
MARK(and(X1, X2)) → A__AND(mark(X1), X2)
A____(__(X, Y), Z) → MARK(X)
MARK(and(X1, X2)) → MARK(X1)
A____(nil, X) → MARK(X)
A____(X, nil) → MARK(X)
MARK(__(X1, X2)) → A____(mark(X1), mark(X2))
A____(__(X, Y), Z) → MARK(Y)
MARK(__(X1, X2)) → MARK(X2)
a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__and(tt, X) → mark(X)
a__isNePal(__(I, __(P, I))) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNePal(X)) → a__isNePal(mark(X))
mark(nil) → nil
mark(tt) → tt
a____(X1, X2) → __(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNePal(X) → isNePal(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
A____(__(X, Y), Z) → A____(mark(X), a____(mark(Y), mark(Z)))
A____(__(X, Y), Z) → MARK(Z)
A____(__(X, Y), Z) → A____(mark(Y), mark(Z))
MARK(__(X1, X2)) → MARK(X1)
MARK(and(X1, X2)) → A__AND(mark(X1), X2)
A____(__(X, Y), Z) → MARK(X)
MARK(and(X1, X2)) → MARK(X1)
MARK(__(X1, X2)) → A____(mark(X1), mark(X2))
A____(__(X, Y), Z) → MARK(Y)
MARK(__(X1, X2)) → MARK(X2)
Used ordering: Polynomial interpretation [25,35]:
MARK(isNePal(X)) → MARK(X)
A__AND(tt, X) → MARK(X)
A____(nil, X) → MARK(X)
A____(X, nil) → MARK(X)
The value of delta used in the strict ordering is 1.
POL(a____(x1, x2)) = 4 + (4)x_1 + x_2
POL(A__AND(x1, x2)) = x_2
POL(A____(x1, x2)) = (4)x_1 + x_2
POL(MARK(x1)) = x_1
POL(__(x1, x2)) = 4 + (4)x_1 + x_2
POL(tt) = 2
POL(a__and(x1, x2)) = 1 + (4)x_1 + (2)x_2
POL(a__isNePal(x1)) = (2)x_1
POL(mark(x1)) = x_1
POL(isNePal(x1)) = (2)x_1
POL(and(x1, x2)) = 1 + (4)x_1 + (2)x_2
POL(nil) = 0
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
mark(and(X1, X2)) → a__and(mark(X1), X2)
a__and(tt, X) → mark(X)
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__isNePal(__(I, __(P, I))) → tt
mark(isNePal(X)) → a__isNePal(mark(X))
mark(tt) → tt
mark(nil) → nil
a__and(X1, X2) → and(X1, X2)
a____(X1, X2) → __(X1, X2)
a__isNePal(X) → isNePal(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
MARK(isNePal(X)) → MARK(X)
A____(X, nil) → MARK(X)
A____(nil, X) → MARK(X)
A__AND(tt, X) → MARK(X)
a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__and(tt, X) → mark(X)
a__isNePal(__(I, __(P, I))) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNePal(X)) → a__isNePal(mark(X))
mark(nil) → nil
mark(tt) → tt
a____(X1, X2) → __(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNePal(X) → isNePal(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
MARK(isNePal(X)) → MARK(X)
a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__and(tt, X) → mark(X)
a__isNePal(__(I, __(P, I))) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNePal(X)) → a__isNePal(mark(X))
mark(nil) → nil
mark(tt) → tt
a____(X1, X2) → __(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNePal(X) → isNePal(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(isNePal(X)) → MARK(X)
The value of delta used in the strict ordering is 4.
POL(MARK(x1)) = (4)x_1
POL(isNePal(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
a____(__(X, Y), Z) → a____(mark(X), a____(mark(Y), mark(Z)))
a____(X, nil) → mark(X)
a____(nil, X) → mark(X)
a__and(tt, X) → mark(X)
a__isNePal(__(I, __(P, I))) → tt
mark(__(X1, X2)) → a____(mark(X1), mark(X2))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNePal(X)) → a__isNePal(mark(X))
mark(nil) → nil
mark(tt) → tt
a____(X1, X2) → __(X1, X2)
a__and(X1, X2) → and(X1, X2)
a__isNePal(X) → isNePal(X)