Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

a__U41^#(tt, M, N)	→	a__plus^#(mark(N), mark(M))	mark^#(isNat(X))	→	a__isNat^#(X)
a__U11^#(tt, V1, V2)	→	a__isNat^#(V1)	a__U31^#(tt, N)	→	mark^#(N)
a__U12^#(tt, V2)	→	a__isNat^#(V2)	mark^#(U21(X1, X2))	→	mark^#(X1)
a__plus^#(N, 0)	→	a__and^#(a__isNat(N), isNatKind(N))	mark^#(U31(X1, X2))	→	a__U31^#(mark(X1), X2)
mark^#(U41(X1, X2, X3))	→	a__U41^#(mark(X1), X2, X3)	a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)
a__U41^#(tt, M, N)	→	mark^#(M)	a__U21^#(tt, V1)	→	a__U22^#(a__isNat(V1))
mark^#(U13(X))	→	a__U13^#(mark(X))	mark^#(plus(X1, X2))	→	mark^#(X2)
mark^#(U22(X))	→	a__U22^#(mark(X))	a__and^#(tt, X)	→	mark^#(X)
a__plus^#(N, s(M))	→	a__U41^#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)	mark^#(U31(X1, X2))	→	mark^#(X1)
a__plus^#(N, s(M))	→	a__isNat^#(M)	a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))
mark^#(s(X))	→	mark^#(X)	a__isNat^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))
a__plus^#(N, s(M))	→	a__and^#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))	a__isNat^#(plus(V1, V2))	→	a__U11^#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
mark^#(U12(X1, X2))	→	mark^#(X1)	a__U21^#(tt, V1)	→	a__isNat^#(V1)
a__plus^#(N, s(M))	→	a__and^#(a__isNat(M), isNatKind(M))	a__U12^#(tt, V2)	→	a__U13^#(a__isNat(V2))
mark^#(plus(X1, X2))	→	a__plus^#(mark(X1), mark(X2))	a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	a__U11^#(tt, V1, V2)	→	a__U12^#(a__isNat(V1), V2)
a__plus^#(N, 0)	→	a__U31^#(a__and(a__isNat(N), isNatKind(N)), N)	mark^#(plus(X1, X2))	→	mark^#(X1)
mark^#(and(X1, X2))	→	mark^#(X1)	mark^#(U22(X))	→	mark^#(X)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1), V1)	mark^#(U41(X1, X2, X3))	→	mark^#(X1)
mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)	mark^#(U21(X1, X2))	→	a__U21^#(mark(X1), X2)
a__isNat^#(plus(V1, V2))	→	a__isNatKind^#(V1)	mark^#(U12(X1, X2))	→	a__U12^#(mark(X1), X2)
a__plus^#(N, 0)	→	a__isNat^#(N)	a__U41^#(tt, M, N)	→	mark^#(N)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	mark^#(U11(X1, X2, X3))	→	a__U11^#(mark(X1), X2, X3)
mark^#(U11(X1, X2, X3))	→	mark^#(X1)	mark^#(U13(X))	→	mark^#(X)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Termination of terms over the following signature is verified: a__and, isNat, U41, a__U41, a__U22, U21, a__U21, U22, plus, isNatKind, a__plus, mark, and, 0, s, tt, a__isNat, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__isNatKind

Strategy

The following SCCs where found

a__U41^#(tt, M, N) → a__plus^#(mark(N), mark(M))	mark^#(isNat(X)) → a__isNat^#(X)
a__U11^#(tt, V1, V2) → a__isNat^#(V1)	a__U31^#(tt, N) → mark^#(N)
a__U12^#(tt, V2) → a__isNat^#(V2)	mark^#(U21(X1, X2)) → mark^#(X1)
mark^#(U31(X1, X2)) → a__U31^#(mark(X1), X2)	mark^#(U41(X1, X2, X3)) → a__U41^#(mark(X1), X2, X3)
a__plus^#(N, 0) → a__and^#(a__isNat(N), isNatKind(N))	a__isNatKind^#(s(V1)) → a__isNatKind^#(V1)
a__U41^#(tt, M, N) → mark^#(M)	mark^#(plus(X1, X2)) → mark^#(X2)
a__and^#(tt, X) → mark^#(X)	a__plus^#(N, s(M)) → a__U41^#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__isNatKind^#(plus(V1, V2)) → a__and^#(a__isNatKind(V1), isNatKind(V2))	mark^#(U31(X1, X2)) → mark^#(X1)
a__plus^#(N, s(M)) → a__isNat^#(M)	a__plus^#(N, s(M)) → a__and^#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))
mark^#(s(X)) → mark^#(X)	a__isNat^#(plus(V1, V2)) → a__and^#(a__isNatKind(V1), isNatKind(V2))
a__isNat^#(plus(V1, V2)) → a__U11^#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	mark^#(U12(X1, X2)) → mark^#(X1)
a__U21^#(tt, V1) → a__isNat^#(V1)	a__plus^#(N, s(M)) → a__and^#(a__isNat(M), isNatKind(M))
mark^#(plus(X1, X2)) → a__plus^#(mark(X1), mark(X2))	a__isNatKind^#(plus(V1, V2)) → a__isNatKind^#(V1)
a__isNat^#(s(V1)) → a__isNatKind^#(V1)	a__U11^#(tt, V1, V2) → a__U12^#(a__isNat(V1), V2)
mark^#(plus(X1, X2)) → mark^#(X1)	a__plus^#(N, 0) → a__U31^#(a__and(a__isNat(N), isNatKind(N)), N)
mark^#(and(X1, X2)) → mark^#(X1)	mark^#(U22(X)) → mark^#(X)
mark^#(U41(X1, X2, X3)) → mark^#(X1)	mark^#(and(X1, X2)) → a__and^#(mark(X1), X2)
a__isNat^#(s(V1)) → a__U21^#(a__isNatKind(V1), V1)	mark^#(U21(X1, X2)) → a__U21^#(mark(X1), X2)
mark^#(U12(X1, X2)) → a__U12^#(mark(X1), X2)	a__isNat^#(plus(V1, V2)) → a__isNatKind^#(V1)
a__U41^#(tt, M, N) → mark^#(N)	a__plus^#(N, 0) → a__isNat^#(N)
mark^#(isNatKind(X)) → a__isNatKind^#(X)	mark^#(U11(X1, X2, X3)) → a__U11^#(mark(X1), X2, X3)
mark^#(U11(X1, X2, X3)) → mark^#(X1)	mark^#(U13(X)) → mark^#(X)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

a__U41^#(tt, M, N)	→	a__plus^#(mark(N), mark(M))	mark^#(isNat(X))	→	a__isNat^#(X)
a__U11^#(tt, V1, V2)	→	a__isNat^#(V1)	a__U31^#(tt, N)	→	mark^#(N)
a__U12^#(tt, V2)	→	a__isNat^#(V2)	mark^#(U21(X1, X2))	→	mark^#(X1)
mark^#(U31(X1, X2))	→	a__U31^#(mark(X1), X2)	mark^#(U41(X1, X2, X3))	→	a__U41^#(mark(X1), X2, X3)
a__plus^#(N, 0)	→	a__and^#(a__isNat(N), isNatKind(N))	a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)
a__U41^#(tt, M, N)	→	mark^#(M)	mark^#(plus(X1, X2))	→	mark^#(X2)
a__plus^#(N, s(M))	→	a__U41^#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)	a__and^#(tt, X)	→	mark^#(X)
a__plus^#(N, s(M))	→	a__isNat^#(M)	mark^#(U31(X1, X2))	→	mark^#(X1)
a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))	a__isNat^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))
mark^#(s(X))	→	mark^#(X)	a__plus^#(N, s(M))	→	a__and^#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))
a__isNat^#(plus(V1, V2))	→	a__U11^#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	mark^#(U12(X1, X2))	→	mark^#(X1)
a__U21^#(tt, V1)	→	a__isNat^#(V1)	a__plus^#(N, s(M))	→	a__and^#(a__isNat(M), isNatKind(M))
mark^#(plus(X1, X2))	→	a__plus^#(mark(X1), mark(X2))	a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	a__U11^#(tt, V1, V2)	→	a__U12^#(a__isNat(V1), V2)
mark^#(plus(X1, X2))	→	mark^#(X1)	a__plus^#(N, 0)	→	a__U31^#(a__and(a__isNat(N), isNatKind(N)), N)
mark^#(and(X1, X2))	→	mark^#(X1)	mark^#(U22(X))	→	mark^#(X)
mark^#(U41(X1, X2, X3))	→	mark^#(X1)	mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1), V1)	mark^#(U21(X1, X2))	→	a__U21^#(mark(X1), X2)
mark^#(U12(X1, X2))	→	a__U12^#(mark(X1), X2)	a__isNat^#(plus(V1, V2))	→	a__isNatKind^#(V1)
a__U41^#(tt, M, N)	→	mark^#(N)	a__plus^#(N, 0)	→	a__isNat^#(N)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	mark^#(U11(X1, X2, X3))	→	a__U11^#(mark(X1), X2, X3)
mark^#(U11(X1, X2, X3))	→	mark^#(X1)	mark^#(U13(X))	→	mark^#(X)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Polynomial Interpretation

0: 1
U11(x,y,z): 2x
U12(x,y): x
U13(x): x
U21(x,y): 3x
U22(x): x
U31(x,y): y + x
U41(x,y,z): z + 2y + x
a__U11(x,y,z): 2x
a__U11#(x,y,z): 0
a__U12(x,y): x
a__U12#(x,y): 0
a__U13(x): x
a__U21(x,y): 3x
a__U21#(x,y): 0
a__U22(x): x
a__U31(x,y): y + x
a__U31#(x,y): 2y
a__U41(x,y,z): z + 2y + x
a__U41#(x,y,z): 2z + 2y
a__and(x,y): y + x
a__and#(x,y): 2y
a__isNat(x): 0
a__isNat#(x): 0
a__isNatKind(x): 0
a__isNatKind#(x): 0
a__plus(x,y): 2y + x
a__plus#(x,y): 2y + 2x
and(x,y): y + x
isNat(x): 0
isNatKind(x): 0
mark(x): x
mark#(x): 2x
plus(x,y): 2y + x
s(x): x
tt: 0

Standard Usable rules

a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))
a__U22(tt)	→	tt	mark(isNatKind(X))	→	a__isNatKind(X)
a__isNatKind(0)	→	tt	a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)
a__isNat(0)	→	tt	a__isNat(X)	→	isNat(X)
a__U21(tt, V1)	→	a__U22(a__isNat(V1))	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
a__U31(tt, N)	→	mark(N)	mark(U13(X))	→	a__U13(mark(X))
mark(U22(X))	→	a__U22(mark(X))	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__U12(X1, X2)	→	U12(X1, X2)
a__U13(tt)	→	tt	a__U22(X)	→	U22(X)
mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__U21(X1, X2)	→	U21(X1, X2)	mark(tt)	→	tt
mark(0)	→	0	a__plus(X1, X2)	→	plus(X1, X2)
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	a__and(X1, X2)	→	and(X1, X2)
a__U13(X)	→	U13(X)	a__and(tt, X)	→	mark(X)
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(isNat(X))	→	a__isNat(X)
a__U41(X1, X2, X3)	→	U41(X1, X2, X3)	mark(and(X1, X2))	→	a__and(mark(X1), X2)
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)
mark(s(X))	→	s(mark(X))	a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__U31(X1, X2)	→	U31(X1, X2)	mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__isNatKind(X)	→	isNatKind(X)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

a__plus^#(N, 0)	→	a__and^#(a__isNat(N), isNatKind(N))		a__plus^#(N, 0)	→	a__U31^#(a__and(a__isNat(N), isNatKind(N)), N)
a__plus^#(N, 0)	→	a__isNat^#(N)

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

a__U41^#(tt, M, N)	→	a__plus^#(mark(N), mark(M))	mark^#(isNat(X))	→	a__isNat^#(X)
a__U11^#(tt, V1, V2)	→	a__isNat^#(V1)	a__U31^#(tt, N)	→	mark^#(N)
a__U12^#(tt, V2)	→	a__isNat^#(V2)	mark^#(U21(X1, X2))	→	mark^#(X1)
mark^#(U41(X1, X2, X3))	→	a__U41^#(mark(X1), X2, X3)	mark^#(U31(X1, X2))	→	a__U31^#(mark(X1), X2)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	a__U41^#(tt, M, N)	→	mark^#(M)
mark^#(plus(X1, X2))	→	mark^#(X2)	a__and^#(tt, X)	→	mark^#(X)
a__plus^#(N, s(M))	→	a__U41^#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)	a__plus^#(N, s(M))	→	a__isNat^#(M)
mark^#(U31(X1, X2))	→	mark^#(X1)	a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))
a__isNat^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))	mark^#(s(X))	→	mark^#(X)
a__plus^#(N, s(M))	→	a__and^#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))	a__isNat^#(plus(V1, V2))	→	a__U11^#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
mark^#(U12(X1, X2))	→	mark^#(X1)	a__U21^#(tt, V1)	→	a__isNat^#(V1)
a__plus^#(N, s(M))	→	a__and^#(a__isNat(M), isNatKind(M))	mark^#(plus(X1, X2))	→	a__plus^#(mark(X1), mark(X2))
a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)	a__U11^#(tt, V1, V2)	→	a__U12^#(a__isNat(V1), V2)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	mark^#(plus(X1, X2))	→	mark^#(X1)
mark^#(and(X1, X2))	→	mark^#(X1)	mark^#(U22(X))	→	mark^#(X)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1), V1)	mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)
mark^#(U41(X1, X2, X3))	→	mark^#(X1)	mark^#(U21(X1, X2))	→	a__U21^#(mark(X1), X2)
a__isNat^#(plus(V1, V2))	→	a__isNatKind^#(V1)	mark^#(U12(X1, X2))	→	a__U12^#(mark(X1), X2)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	a__U41^#(tt, M, N)	→	mark^#(N)
mark^#(U11(X1, X2, X3))	→	a__U11^#(mark(X1), X2, X3)	mark^#(U11(X1, X2, X3))	→	mark^#(X1)
mark^#(U13(X))	→	mark^#(X)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Termination of terms over the following signature is verified: a__and, isNat, U41, a__U41, a__U22, a__U21, U21, U22, plus, isNatKind, a__plus, mark, and, 0, s, tt, a__isNat, a__U31, a__U13, U11, a__U12, U12, a__U11, U13, U31, a__isNatKind

Strategy

Polynomial Interpretation

0: 0
U11(x,y,z): 2x
U12(x,y): x
U13(x): 2x
U21(x,y): x
U22(x): 2x
U31(x,y): y + x
U41(x,y,z): z + y + x + 2
a__U11(x,y,z): 2x
a__U11#(x,y,z): 2x
a__U12(x,y): x
a__U12#(x,y): x
a__U13(x): 2x
a__U21(x,y): x
a__U21#(x,y): x
a__U22(x): 2x
a__U31(x,y): y + x
a__U31#(x,y): y
a__U41(x,y,z): z + y + x + 2
a__U41#(x,y,z): z + y + x
a__and(x,y): 2y + x
a__and#(x,y): y + x
a__isNat(x): 0
a__isNat#(x): 0
a__isNatKind(x): 0
a__isNatKind#(x): 0
a__plus(x,y): y + x + 2
a__plus#(x,y): y + x
and(x,y): 2y + x
isNat(x): 0
isNatKind(x): 0
mark(x): x
mark#(x): x
plus(x,y): y + x + 2
s(x): x
tt: 0

Standard Usable rules

a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))
a__U22(tt)	→	tt	mark(isNatKind(X))	→	a__isNatKind(X)
a__isNatKind(0)	→	tt	a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)
a__isNat(0)	→	tt	a__isNat(X)	→	isNat(X)
a__U21(tt, V1)	→	a__U22(a__isNat(V1))	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
a__U31(tt, N)	→	mark(N)	mark(U13(X))	→	a__U13(mark(X))
mark(U22(X))	→	a__U22(mark(X))	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__U12(X1, X2)	→	U12(X1, X2)
a__U13(tt)	→	tt	a__U22(X)	→	U22(X)
mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__U21(X1, X2)	→	U21(X1, X2)	mark(tt)	→	tt
mark(0)	→	0	a__plus(X1, X2)	→	plus(X1, X2)
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	a__and(X1, X2)	→	and(X1, X2)
a__U13(X)	→	U13(X)	a__and(tt, X)	→	mark(X)
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(isNat(X))	→	a__isNat(X)
a__U41(X1, X2, X3)	→	U41(X1, X2, X3)	mark(and(X1, X2))	→	a__and(mark(X1), X2)
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)
mark(s(X))	→	s(mark(X))	a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__U31(X1, X2)	→	U31(X1, X2)	mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__isNatKind(X)	→	isNatKind(X)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

mark^#(U41(X1, X2, X3))	→	a__U41^#(mark(X1), X2, X3)	mark^#(plus(X1, X2))	→	mark^#(X2)
mark^#(plus(X1, X2))	→	a__plus^#(mark(X1), mark(X2))	mark^#(plus(X1, X2))	→	mark^#(X1)
mark^#(U41(X1, X2, X3))	→	mark^#(X1)

Problem 4: DependencyGraph

Dependency Pair Problem

Dependency Pairs

a__U41^#(tt, M, N)	→	a__plus^#(mark(N), mark(M))	mark^#(isNat(X))	→	a__isNat^#(X)
a__U11^#(tt, V1, V2)	→	a__isNat^#(V1)	a__U31^#(tt, N)	→	mark^#(N)
a__U12^#(tt, V2)	→	a__isNat^#(V2)	mark^#(U21(X1, X2))	→	mark^#(X1)
mark^#(U31(X1, X2))	→	a__U31^#(mark(X1), X2)	a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)
a__U41^#(tt, M, N)	→	mark^#(M)	a__plus^#(N, s(M))	→	a__U41^#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__and^#(tt, X)	→	mark^#(X)	mark^#(U31(X1, X2))	→	mark^#(X1)
a__plus^#(N, s(M))	→	a__isNat^#(M)	a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))
a__isNat^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))	mark^#(s(X))	→	mark^#(X)
a__plus^#(N, s(M))	→	a__and^#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))	a__isNat^#(plus(V1, V2))	→	a__U11^#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
mark^#(U12(X1, X2))	→	mark^#(X1)	a__U21^#(tt, V1)	→	a__isNat^#(V1)
a__plus^#(N, s(M))	→	a__and^#(a__isNat(M), isNatKind(M))	a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)
a__U11^#(tt, V1, V2)	→	a__U12^#(a__isNat(V1), V2)	a__isNat^#(s(V1))	→	a__isNatKind^#(V1)
mark^#(and(X1, X2))	→	mark^#(X1)	mark^#(U22(X))	→	mark^#(X)
mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)	a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1), V1)
mark^#(U21(X1, X2))	→	a__U21^#(mark(X1), X2)	mark^#(U12(X1, X2))	→	a__U12^#(mark(X1), X2)
a__isNat^#(plus(V1, V2))	→	a__isNatKind^#(V1)	a__U41^#(tt, M, N)	→	mark^#(N)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	mark^#(U11(X1, X2, X3))	→	a__U11^#(mark(X1), X2, X3)
mark^#(U11(X1, X2, X3))	→	mark^#(X1)	mark^#(U13(X))	→	mark^#(X)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

The following SCCs where found

mark^#(isNat(X)) → a__isNat^#(X)	a__U11^#(tt, V1, V2) → a__isNat^#(V1)
a__U31^#(tt, N) → mark^#(N)	a__U12^#(tt, V2) → a__isNat^#(V2)
mark^#(U21(X1, X2)) → mark^#(X1)	mark^#(U31(X1, X2)) → a__U31^#(mark(X1), X2)
a__isNatKind^#(s(V1)) → a__isNatKind^#(V1)	a__and^#(tt, X) → mark^#(X)
mark^#(U31(X1, X2)) → mark^#(X1)	a__isNatKind^#(plus(V1, V2)) → a__and^#(a__isNatKind(V1), isNatKind(V2))
mark^#(s(X)) → mark^#(X)	a__isNat^#(plus(V1, V2)) → a__and^#(a__isNatKind(V1), isNatKind(V2))
a__isNat^#(plus(V1, V2)) → a__U11^#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	mark^#(U12(X1, X2)) → mark^#(X1)
a__U21^#(tt, V1) → a__isNat^#(V1)	a__isNatKind^#(plus(V1, V2)) → a__isNatKind^#(V1)
a__isNat^#(s(V1)) → a__isNatKind^#(V1)	a__U11^#(tt, V1, V2) → a__U12^#(a__isNat(V1), V2)
mark^#(and(X1, X2)) → mark^#(X1)	mark^#(U22(X)) → mark^#(X)
mark^#(and(X1, X2)) → a__and^#(mark(X1), X2)	a__isNat^#(s(V1)) → a__U21^#(a__isNatKind(V1), V1)
mark^#(U21(X1, X2)) → a__U21^#(mark(X1), X2)	mark^#(U12(X1, X2)) → a__U12^#(mark(X1), X2)
a__isNat^#(plus(V1, V2)) → a__isNatKind^#(V1)	mark^#(isNatKind(X)) → a__isNatKind^#(X)
mark^#(U11(X1, X2, X3)) → a__U11^#(mark(X1), X2, X3)	mark^#(U11(X1, X2, X3)) → mark^#(X1)
mark^#(U13(X)) → mark^#(X)

a__U41^#(tt, M, N) → a__plus^#(mark(N), mark(M))

a__plus^#(N, s(M)) → a__U41^#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)

Problem 5: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark^#(isNat(X))	→	a__isNat^#(X)	a__U11^#(tt, V1, V2)	→	a__isNat^#(V1)
a__U31^#(tt, N)	→	mark^#(N)	a__U12^#(tt, V2)	→	a__isNat^#(V2)
mark^#(U21(X1, X2))	→	mark^#(X1)	mark^#(U31(X1, X2))	→	a__U31^#(mark(X1), X2)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	a__and^#(tt, X)	→	mark^#(X)
mark^#(U31(X1, X2))	→	mark^#(X1)	a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))
mark^#(s(X))	→	mark^#(X)	a__isNat^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))
a__isNat^#(plus(V1, V2))	→	a__U11^#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	mark^#(U12(X1, X2))	→	mark^#(X1)
a__U21^#(tt, V1)	→	a__isNat^#(V1)	a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)
a__U11^#(tt, V1, V2)	→	a__U12^#(a__isNat(V1), V2)	a__isNat^#(s(V1))	→	a__isNatKind^#(V1)
mark^#(and(X1, X2))	→	mark^#(X1)	mark^#(U22(X))	→	mark^#(X)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1), V1)	mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)
mark^#(U21(X1, X2))	→	a__U21^#(mark(X1), X2)	a__isNat^#(plus(V1, V2))	→	a__isNatKind^#(V1)
mark^#(U12(X1, X2))	→	a__U12^#(mark(X1), X2)	mark^#(isNatKind(X))	→	a__isNatKind^#(X)
mark^#(U11(X1, X2, X3))	→	a__U11^#(mark(X1), X2, X3)	mark^#(U11(X1, X2, X3))	→	mark^#(X1)
mark^#(U13(X))	→	mark^#(X)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Polynomial Interpretation

0: 2
U11(x,y,z): 2x
U12(x,y): 2x
U13(x): x
U21(x,y): x
U22(x): x
U31(x,y): y + 2x + 1
U41(x,y,z): z + y
a__U11(x,y,z): 2x
a__U11#(x,y,z): 0
a__U12(x,y): 2x
a__U12#(x,y): 0
a__U13(x): x
a__U21(x,y): x
a__U21#(x,y): 0
a__U22(x): x
a__U31(x,y): y + 2x + 1
a__U31#(x,y): 2y
a__U41(x,y,z): z + y
a__and(x,y): y + 2x
a__and#(x,y): 2y
a__isNat(x): 0
a__isNat#(x): 0
a__isNatKind(x): 0
a__isNatKind#(x): 0
a__plus(x,y): y + x
and(x,y): y + 2x
isNat(x): 0
isNatKind(x): 0
mark(x): x
mark#(x): 2x
plus(x,y): y + x
s(x): x
tt: 0

Standard Usable rules

a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))
a__U22(tt)	→	tt	mark(isNatKind(X))	→	a__isNatKind(X)
a__isNatKind(0)	→	tt	a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)
a__isNat(0)	→	tt	a__isNat(X)	→	isNat(X)
a__U21(tt, V1)	→	a__U22(a__isNat(V1))	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
a__U31(tt, N)	→	mark(N)	mark(U13(X))	→	a__U13(mark(X))
mark(U22(X))	→	a__U22(mark(X))	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__U12(X1, X2)	→	U12(X1, X2)
a__U13(tt)	→	tt	a__U22(X)	→	U22(X)
mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__U21(X1, X2)	→	U21(X1, X2)	mark(tt)	→	tt
mark(0)	→	0	a__plus(X1, X2)	→	plus(X1, X2)
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	a__and(X1, X2)	→	and(X1, X2)
a__U13(X)	→	U13(X)	a__and(tt, X)	→	mark(X)
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(isNat(X))	→	a__isNat(X)
a__U41(X1, X2, X3)	→	U41(X1, X2, X3)	mark(and(X1, X2))	→	a__and(mark(X1), X2)
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)
mark(s(X))	→	s(mark(X))	a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__U31(X1, X2)	→	U31(X1, X2)	mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__isNatKind(X)	→	isNatKind(X)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

mark^#(U31(X1, X2))

→

a__U31^#(mark(X1), X2)

mark^#(U31(X1, X2))

→

mark^#(X1)

Problem 7: DependencyGraph

Dependency Pair Problem

Dependency Pairs

mark^#(isNat(X))	→	a__isNat^#(X)	a__U11^#(tt, V1, V2)	→	a__isNat^#(V1)
a__U31^#(tt, N)	→	mark^#(N)	a__U12^#(tt, V2)	→	a__isNat^#(V2)
mark^#(U21(X1, X2))	→	mark^#(X1)	a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)
a__and^#(tt, X)	→	mark^#(X)	a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))
a__isNat^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))	mark^#(s(X))	→	mark^#(X)
a__isNat^#(plus(V1, V2))	→	a__U11^#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	mark^#(U12(X1, X2))	→	mark^#(X1)
a__U21^#(tt, V1)	→	a__isNat^#(V1)	a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)
a__U11^#(tt, V1, V2)	→	a__U12^#(a__isNat(V1), V2)	a__isNat^#(s(V1))	→	a__isNatKind^#(V1)
mark^#(and(X1, X2))	→	mark^#(X1)	mark^#(U22(X))	→	mark^#(X)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1), V1)	mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)
mark^#(U21(X1, X2))	→	a__U21^#(mark(X1), X2)	a__isNat^#(plus(V1, V2))	→	a__isNatKind^#(V1)
mark^#(U12(X1, X2))	→	a__U12^#(mark(X1), X2)	mark^#(isNatKind(X))	→	a__isNatKind^#(X)
mark^#(U11(X1, X2, X3))	→	a__U11^#(mark(X1), X2, X3)	mark^#(U11(X1, X2, X3))	→	mark^#(X1)
mark^#(U13(X))	→	mark^#(X)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

The following SCCs where found

mark^#(isNat(X)) → a__isNat^#(X)	a__U11^#(tt, V1, V2) → a__isNat^#(V1)
a__U12^#(tt, V2) → a__isNat^#(V2)	mark^#(U21(X1, X2)) → mark^#(X1)
a__isNatKind^#(s(V1)) → a__isNatKind^#(V1)	a__and^#(tt, X) → mark^#(X)
a__isNatKind^#(plus(V1, V2)) → a__and^#(a__isNatKind(V1), isNatKind(V2))	mark^#(s(X)) → mark^#(X)
a__isNat^#(plus(V1, V2)) → a__and^#(a__isNatKind(V1), isNatKind(V2))	a__isNat^#(plus(V1, V2)) → a__U11^#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
mark^#(U12(X1, X2)) → mark^#(X1)	a__U21^#(tt, V1) → a__isNat^#(V1)
a__isNatKind^#(plus(V1, V2)) → a__isNatKind^#(V1)	a__isNat^#(s(V1)) → a__isNatKind^#(V1)
a__U11^#(tt, V1, V2) → a__U12^#(a__isNat(V1), V2)	mark^#(and(X1, X2)) → mark^#(X1)
mark^#(U22(X)) → mark^#(X)	mark^#(and(X1, X2)) → a__and^#(mark(X1), X2)
a__isNat^#(s(V1)) → a__U21^#(a__isNatKind(V1), V1)	mark^#(U21(X1, X2)) → a__U21^#(mark(X1), X2)
a__isNat^#(plus(V1, V2)) → a__isNatKind^#(V1)	mark^#(U12(X1, X2)) → a__U12^#(mark(X1), X2)
mark^#(isNatKind(X)) → a__isNatKind^#(X)	mark^#(U11(X1, X2, X3)) → a__U11^#(mark(X1), X2, X3)
mark^#(U11(X1, X2, X3)) → mark^#(X1)	mark^#(U13(X)) → mark^#(X)

Problem 9: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark^#(isNat(X))	→	a__isNat^#(X)	a__U11^#(tt, V1, V2)	→	a__isNat^#(V1)
a__U12^#(tt, V2)	→	a__isNat^#(V2)	mark^#(U21(X1, X2))	→	mark^#(X1)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	a__and^#(tt, X)	→	mark^#(X)
a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))	mark^#(s(X))	→	mark^#(X)
a__isNat^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))	a__isNat^#(plus(V1, V2))	→	a__U11^#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
mark^#(U12(X1, X2))	→	mark^#(X1)	a__U21^#(tt, V1)	→	a__isNat^#(V1)
a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)	a__U11^#(tt, V1, V2)	→	a__U12^#(a__isNat(V1), V2)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	mark^#(and(X1, X2))	→	mark^#(X1)
mark^#(U22(X))	→	mark^#(X)	a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1), V1)
mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)	mark^#(U21(X1, X2))	→	a__U21^#(mark(X1), X2)
mark^#(U12(X1, X2))	→	a__U12^#(mark(X1), X2)	a__isNat^#(plus(V1, V2))	→	a__isNatKind^#(V1)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	mark^#(U11(X1, X2, X3))	→	a__U11^#(mark(X1), X2, X3)
mark^#(U11(X1, X2, X3))	→	mark^#(X1)	mark^#(U13(X))	→	mark^#(X)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Polynomial Interpretation

0: 0
U11(x,y,z): 2x
U12(x,y): x
U13(x): x
U21(x,y): x
U22(x): 2x
U31(x,y): y
U41(x,y,z): z + y + 2
a__U11(x,y,z): 2x
a__U11#(x,y,z): 0
a__U12(x,y): x
a__U12#(x,y): 0
a__U13(x): x
a__U21(x,y): x
a__U21#(x,y): 0
a__U22(x): 2x
a__U31(x,y): y
a__U41(x,y,z): z + y + 2
a__and(x,y): y + 2x
a__and#(x,y): y
a__isNat(x): 0
a__isNat#(x): 0
a__isNatKind(x): 0
a__isNatKind#(x): 0
a__plus(x,y): y + x + 1
and(x,y): y + 2x
isNat(x): 0
isNatKind(x): 0
mark(x): x
mark#(x): x
plus(x,y): y + x + 1
s(x): x + 1
tt: 0

Standard Usable rules

a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))
a__U22(tt)	→	tt	mark(isNatKind(X))	→	a__isNatKind(X)
a__isNatKind(0)	→	tt	a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)
a__isNat(0)	→	tt	a__isNat(X)	→	isNat(X)
a__U21(tt, V1)	→	a__U22(a__isNat(V1))	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
a__U31(tt, N)	→	mark(N)	mark(U13(X))	→	a__U13(mark(X))
mark(U22(X))	→	a__U22(mark(X))	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__U12(X1, X2)	→	U12(X1, X2)
a__U13(tt)	→	tt	a__U22(X)	→	U22(X)
mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__U21(X1, X2)	→	U21(X1, X2)	mark(tt)	→	tt
mark(0)	→	0	a__plus(X1, X2)	→	plus(X1, X2)
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	a__and(X1, X2)	→	and(X1, X2)
a__U13(X)	→	U13(X)	a__and(tt, X)	→	mark(X)
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(isNat(X))	→	a__isNat(X)
a__U41(X1, X2, X3)	→	U41(X1, X2, X3)	mark(and(X1, X2))	→	a__and(mark(X1), X2)
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)
mark(s(X))	→	s(mark(X))	a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__U31(X1, X2)	→	U31(X1, X2)	mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__isNatKind(X)	→	isNatKind(X)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

mark^#(s(X))

→

mark^#(X)

Problem 10: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark^#(isNat(X))	→	a__isNat^#(X)	a__U11^#(tt, V1, V2)	→	a__isNat^#(V1)
a__U12^#(tt, V2)	→	a__isNat^#(V2)	mark^#(U21(X1, X2))	→	mark^#(X1)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	a__and^#(tt, X)	→	mark^#(X)
a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))	a__isNat^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))
a__isNat^#(plus(V1, V2))	→	a__U11^#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	mark^#(U12(X1, X2))	→	mark^#(X1)
a__U21^#(tt, V1)	→	a__isNat^#(V1)	a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)
a__U11^#(tt, V1, V2)	→	a__U12^#(a__isNat(V1), V2)	a__isNat^#(s(V1))	→	a__isNatKind^#(V1)
mark^#(and(X1, X2))	→	mark^#(X1)	mark^#(U22(X))	→	mark^#(X)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1), V1)	mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)
mark^#(U21(X1, X2))	→	a__U21^#(mark(X1), X2)	mark^#(U12(X1, X2))	→	a__U12^#(mark(X1), X2)
a__isNat^#(plus(V1, V2))	→	a__isNatKind^#(V1)	mark^#(isNatKind(X))	→	a__isNatKind^#(X)
mark^#(U11(X1, X2, X3))	→	a__U11^#(mark(X1), X2, X3)	mark^#(U11(X1, X2, X3))	→	mark^#(X1)
mark^#(U13(X))	→	mark^#(X)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Polynomial Interpretation

0: 0
U11(x,y,z): x
U12(x,y): x
U13(x): x
U21(x,y): x
U22(x): x
U31(x,y): y
U41(x,y,z): z
a__U11(x,y,z): x
a__U11#(x,y,z): 0
a__U12(x,y): x
a__U12#(x,y): 0
a__U13(x): x
a__U21(x,y): x
a__U21#(x,y): 0
a__U22(x): x
a__U31(x,y): 2y + 1
a__U41(x,y,z): z
a__and(x,y): 2y + x
a__and#(x,y): 2y
a__isNat(x): 1
a__isNat#(x): 0
a__isNatKind(x): 1
a__isNatKind#(x): 0
a__plus(x,y): 2x + 1
and(x,y): y + x
isNat(x): 1
isNatKind(x): 0
mark(x): 2x + 1
mark#(x): 2x
plus(x,y): 2x + 1
s(x): 0
tt: 1

Standard Usable rules

a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))
a__U22(tt)	→	tt	mark(isNatKind(X))	→	a__isNatKind(X)
a__isNatKind(0)	→	tt	a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)
a__isNat(0)	→	tt	a__isNat(X)	→	isNat(X)
a__U21(tt, V1)	→	a__U22(a__isNat(V1))	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
a__U31(tt, N)	→	mark(N)	mark(U13(X))	→	a__U13(mark(X))
mark(U22(X))	→	a__U22(mark(X))	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__U12(X1, X2)	→	U12(X1, X2)
a__U13(tt)	→	tt	a__U22(X)	→	U22(X)
mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__U21(X1, X2)	→	U21(X1, X2)	mark(tt)	→	tt
mark(0)	→	0	a__plus(X1, X2)	→	plus(X1, X2)
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	a__and(X1, X2)	→	and(X1, X2)
a__U13(X)	→	U13(X)	a__and(tt, X)	→	mark(X)
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(isNat(X))	→	a__isNat(X)
a__U41(X1, X2, X3)	→	U41(X1, X2, X3)	mark(and(X1, X2))	→	a__and(mark(X1), X2)
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)
mark(s(X))	→	s(mark(X))	a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__U31(X1, X2)	→	U31(X1, X2)	mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__isNatKind(X)	→	isNatKind(X)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

mark^#(isNat(X))

→

a__isNat^#(X)

Problem 11: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

a__U11^#(tt, V1, V2)	→	a__isNat^#(V1)	a__U12^#(tt, V2)	→	a__isNat^#(V2)
mark^#(U21(X1, X2))	→	mark^#(X1)	a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)
a__U11^#(tt, V1, V2)	→	a__U12^#(a__isNat(V1), V2)	a__isNat^#(s(V1))	→	a__isNatKind^#(V1)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	mark^#(and(X1, X2))	→	mark^#(X1)
mark^#(U22(X))	→	mark^#(X)	mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1), V1)	mark^#(U21(X1, X2))	→	a__U21^#(mark(X1), X2)
a__isNat^#(plus(V1, V2))	→	a__isNatKind^#(V1)	mark^#(U12(X1, X2))	→	a__U12^#(mark(X1), X2)
a__and^#(tt, X)	→	mark^#(X)	mark^#(isNatKind(X))	→	a__isNatKind^#(X)
a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))	a__isNat^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))
mark^#(U11(X1, X2, X3))	→	a__U11^#(mark(X1), X2, X3)	a__isNat^#(plus(V1, V2))	→	a__U11^#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
mark^#(U11(X1, X2, X3))	→	mark^#(X1)	mark^#(U12(X1, X2))	→	mark^#(X1)
mark^#(U13(X))	→	mark^#(X)	a__U21^#(tt, V1)	→	a__isNat^#(V1)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Polynomial Interpretation

0: 1
U11(x,y,z): 2z + 2y + x
U12(x,y): 2y + x
U13(x): x
U21(x,y): 2y + 2x + 1
U22(x): x + 1
U31(x,y): y
U41(x,y,z): z + 2y + 2
a__U11(x,y,z): 2z + 2y + x
a__U11#(x,y,z): 3z + 2y
a__U12(x,y): 2y + x
a__U12#(x,y): 2y
a__U13(x): x
a__U21(x,y): 2y + 2x + 1
a__U21#(x,y): 2y
a__U22(x): x + 1
a__U31(x,y): y
a__U41(x,y,z): z + 2y + 2
a__and(x,y): y + 2x
a__and#(x,y): 2y
a__isNat(x): 2x
a__isNat#(x): 2x
a__isNatKind(x): 0
a__isNatKind#(x): 0
a__plus(x,y): 2y + x + 1
and(x,y): y + 2x
isNat(x): 2x
isNatKind(x): 0
mark(x): x
mark#(x): 2x
plus(x,y): 2y + x + 1
s(x): x + 1
tt: 0

Standard Usable rules

a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))
a__U22(tt)	→	tt	mark(isNatKind(X))	→	a__isNatKind(X)
a__isNatKind(0)	→	tt	a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)
a__isNat(0)	→	tt	a__isNat(X)	→	isNat(X)
a__U21(tt, V1)	→	a__U22(a__isNat(V1))	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
a__U31(tt, N)	→	mark(N)	mark(U13(X))	→	a__U13(mark(X))
mark(U22(X))	→	a__U22(mark(X))	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__U12(X1, X2)	→	U12(X1, X2)
a__U13(tt)	→	tt	a__U22(X)	→	U22(X)
mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__U21(X1, X2)	→	U21(X1, X2)	mark(tt)	→	tt
mark(0)	→	0	a__plus(X1, X2)	→	plus(X1, X2)
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	a__and(X1, X2)	→	and(X1, X2)
a__U13(X)	→	U13(X)	a__and(tt, X)	→	mark(X)
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(isNat(X))	→	a__isNat(X)
a__U41(X1, X2, X3)	→	U41(X1, X2, X3)	mark(and(X1, X2))	→	a__and(mark(X1), X2)
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)
mark(s(X))	→	s(mark(X))	a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__U31(X1, X2)	→	U31(X1, X2)	mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__isNatKind(X)	→	isNatKind(X)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

mark^#(U21(X1, X2))	→	mark^#(X1)	a__isNat^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))
a__isNat^#(plus(V1, V2))	→	a__U11^#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__isNat^#(s(V1))	→	a__isNatKind^#(V1)
mark^#(U22(X))	→	mark^#(X)	a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1), V1)
mark^#(U21(X1, X2))	→	a__U21^#(mark(X1), X2)	a__isNat^#(plus(V1, V2))	→	a__isNatKind^#(V1)

Problem 12: DependencyGraph

Dependency Pair Problem

Dependency Pairs

a__U11^#(tt, V1, V2)	→	a__isNat^#(V1)	a__U12^#(tt, V2)	→	a__isNat^#(V2)
a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)	a__U11^#(tt, V1, V2)	→	a__U12^#(a__isNat(V1), V2)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	mark^#(and(X1, X2))	→	mark^#(X1)
mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)	mark^#(U12(X1, X2))	→	a__U12^#(mark(X1), X2)
a__and^#(tt, X)	→	mark^#(X)	mark^#(isNatKind(X))	→	a__isNatKind^#(X)
a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))	mark^#(U11(X1, X2, X3))	→	a__U11^#(mark(X1), X2, X3)
mark^#(U12(X1, X2))	→	mark^#(X1)	mark^#(U11(X1, X2, X3))	→	mark^#(X1)
a__U21^#(tt, V1)	→	a__isNat^#(V1)	mark^#(U13(X))	→	mark^#(X)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

The following SCCs where found

mark^#(and(X1, X2)) → mark^#(X1)	mark^#(and(X1, X2)) → a__and^#(mark(X1), X2)
a__and^#(tt, X) → mark^#(X)	mark^#(isNatKind(X)) → a__isNatKind^#(X)
a__isNatKind^#(plus(V1, V2)) → a__and^#(a__isNatKind(V1), isNatKind(V2))	a__isNatKind^#(plus(V1, V2)) → a__isNatKind^#(V1)
a__isNatKind^#(s(V1)) → a__isNatKind^#(V1)	mark^#(U12(X1, X2)) → mark^#(X1)
mark^#(U11(X1, X2, X3)) → mark^#(X1)	mark^#(U13(X)) → mark^#(X)

Problem 13: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark^#(and(X1, X2))	→	mark^#(X1)	mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)
a__and^#(tt, X)	→	mark^#(X)	mark^#(isNatKind(X))	→	a__isNatKind^#(X)
a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))	a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	mark^#(U12(X1, X2))	→	mark^#(X1)
mark^#(U11(X1, X2, X3))	→	mark^#(X1)	mark^#(U13(X))	→	mark^#(X)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Polynomial Interpretation

0: 0
U11(x,y,z): z + y + x + 1
U12(x,y): y + x
U13(x): x
U21(x,y): 2x
U22(x): 0
U31(x,y): 2y
U41(x,y,z): 1
a__U11(x,y,z): z + y + x + 1
a__U12(x,y): y + x
a__U13(x): x
a__U21(x,y): 2x
a__U22(x): 0
a__U31(x,y): 3y
a__U41(x,y,z): 1
a__and(x,y): 2y + 2x
a__and#(x,y): y
a__isNat(x): x
a__isNatKind(x): 0
a__isNatKind#(x): 0
a__plus(x,y): y + 3x + 2
and(x,y): y + 2x
isNat(x): x
isNatKind(x): 0
mark(x): 2x
mark#(x): x
plus(x,y): y + 3x + 1
s(x): 0
tt: 0

Standard Usable rules

a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))
mark(isNatKind(X))	→	a__isNatKind(X)	a__U22(tt)	→	tt
a__isNatKind(0)	→	tt	a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)
a__isNat(0)	→	tt	a__isNat(X)	→	isNat(X)
a__U21(tt, V1)	→	a__U22(a__isNat(V1))	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
a__U31(tt, N)	→	mark(N)	mark(U13(X))	→	a__U13(mark(X))
mark(U22(X))	→	a__U22(mark(X))	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__U13(tt)	→	tt
a__U12(X1, X2)	→	U12(X1, X2)	a__U22(X)	→	U22(X)
mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__U21(X1, X2)	→	U21(X1, X2)	mark(tt)	→	tt
mark(0)	→	0	a__plus(X1, X2)	→	plus(X1, X2)
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	a__and(X1, X2)	→	and(X1, X2)
a__and(tt, X)	→	mark(X)	a__U13(X)	→	U13(X)
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(isNat(X))	→	a__isNat(X)
a__U41(X1, X2, X3)	→	U41(X1, X2, X3)	mark(and(X1, X2))	→	a__and(mark(X1), X2)
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)
mark(s(X))	→	s(mark(X))	a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__U31(X1, X2)	→	U31(X1, X2)	mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__isNatKind(X)	→	isNatKind(X)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

mark^#(U11(X1, X2, X3))

→

mark^#(X1)

Problem 14: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark^#(and(X1, X2))	→	mark^#(X1)	mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)
a__and^#(tt, X)	→	mark^#(X)	mark^#(isNatKind(X))	→	a__isNatKind^#(X)
a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)	a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	mark^#(U12(X1, X2))	→	mark^#(X1)
mark^#(U13(X))	→	mark^#(X)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Polynomial Interpretation

0: 1
U11(x,y,z): 3z + 3y
U12(x,y): 3y + x
U13(x): x + 1
U21(x,y): 3y
U22(x): x
U31(x,y): 2y
U41(x,y,z): 2z + 2y
a__U11(x,y,z): 3z + 3y
a__U12(x,y): 3y + x
a__U13(x): x + 1
a__U21(x,y): 3y
a__U22(x): x
a__U31(x,y): 2y
a__U41(x,y,z): 2z + 2y
a__and(x,y): 2y + x
a__and#(x,y): y
a__isNat(x): 3x
a__isNatKind(x): 2x
a__isNatKind#(x): x
a__plus(x,y): 2y + 2x
and(x,y): 2y + x
isNat(x): 3x
isNatKind(x): 2x
mark(x): x
mark#(x): x
plus(x,y): 2y + 2x
s(x): x
tt: 2

Standard Usable rules

a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))
mark(isNatKind(X))	→	a__isNatKind(X)	a__U22(tt)	→	tt
a__isNatKind(0)	→	tt	a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)
a__isNat(0)	→	tt	a__isNat(X)	→	isNat(X)
a__U21(tt, V1)	→	a__U22(a__isNat(V1))	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
a__U31(tt, N)	→	mark(N)	mark(U13(X))	→	a__U13(mark(X))
mark(U22(X))	→	a__U22(mark(X))	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__U13(tt)	→	tt
a__U12(X1, X2)	→	U12(X1, X2)	a__U22(X)	→	U22(X)
mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__U21(X1, X2)	→	U21(X1, X2)	mark(tt)	→	tt
mark(0)	→	0	a__plus(X1, X2)	→	plus(X1, X2)
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	a__and(X1, X2)	→	and(X1, X2)
a__and(tt, X)	→	mark(X)	a__U13(X)	→	U13(X)
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(isNat(X))	→	a__isNat(X)
a__U41(X1, X2, X3)	→	U41(X1, X2, X3)	mark(and(X1, X2))	→	a__and(mark(X1), X2)
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)
mark(s(X))	→	s(mark(X))	a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__U31(X1, X2)	→	U31(X1, X2)	mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__isNatKind(X)	→	isNatKind(X)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

mark^#(U13(X))

→

mark^#(X)

Problem 15: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark^#(and(X1, X2))	→	mark^#(X1)	mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)
a__and^#(tt, X)	→	mark^#(X)	mark^#(isNatKind(X))	→	a__isNatKind^#(X)
a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))	a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	mark^#(U12(X1, X2))	→	mark^#(X1)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Polynomial Interpretation

0: 0
U11(x,y,z): y + 2
U12(x,y): x + 1
U13(x): 0
U21(x,y): 0
U22(x): 0
U31(x,y): y + 1
U41(x,y,z): 1
a__U11(x,y,z): y + 2
a__U12(x,y): x + 1
a__U13(x): 0
a__U21(x,y): 0
a__U22(x): 0
a__U31(x,y): y + 1
a__U41(x,y,z): 1
a__and(x,y): 2y + x
a__and#(x,y): 2y + 2x
a__isNat(x): x
a__isNatKind(x): 0
a__isNatKind#(x): 0
a__plus(x,y): x + 2
and(x,y): 2y + x
isNat(x): x
isNatKind(x): 0
mark(x): x
mark#(x): 2x
plus(x,y): x + 2
s(x): 1
tt: 0

Standard Usable rules

a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))
mark(isNatKind(X))	→	a__isNatKind(X)	a__U22(tt)	→	tt
a__isNatKind(0)	→	tt	a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)
a__isNat(0)	→	tt	a__isNat(X)	→	isNat(X)
a__U21(tt, V1)	→	a__U22(a__isNat(V1))	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
a__U31(tt, N)	→	mark(N)	mark(U13(X))	→	a__U13(mark(X))
mark(U22(X))	→	a__U22(mark(X))	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__U13(tt)	→	tt
a__U12(X1, X2)	→	U12(X1, X2)	a__U22(X)	→	U22(X)
mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__U21(X1, X2)	→	U21(X1, X2)	mark(tt)	→	tt
mark(0)	→	0	a__plus(X1, X2)	→	plus(X1, X2)
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	a__and(X1, X2)	→	and(X1, X2)
a__and(tt, X)	→	mark(X)	a__U13(X)	→	U13(X)
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(isNat(X))	→	a__isNat(X)
a__U41(X1, X2, X3)	→	U41(X1, X2, X3)	mark(and(X1, X2))	→	a__and(mark(X1), X2)
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)
mark(s(X))	→	s(mark(X))	a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__U31(X1, X2)	→	U31(X1, X2)	mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__isNatKind(X)	→	isNatKind(X)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

mark^#(U12(X1, X2))

→

mark^#(X1)

Problem 16: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

mark^#(and(X1, X2))	→	mark^#(X1)	mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)
a__and^#(tt, X)	→	mark^#(X)	mark^#(isNatKind(X))	→	a__isNatKind^#(X)
a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)	a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Polynomial Interpretation

0: 0
U11(x,y,z): 0
U12(x,y): 0
U13(x): x
U21(x,y): 0
U22(x): 0
U31(x,y): y
U41(x,y,z): z + 3y + 3
a__U11(x,y,z): 0
a__U12(x,y): 0
a__U13(x): x
a__U21(x,y): 0
a__U22(x): 0
a__U31(x,y): y
a__U41(x,y,z): z + 3y + 3
a__and(x,y): y + x
a__and#(x,y): y
a__isNat(x): 0
a__isNatKind(x): 2x
a__isNatKind#(x): 2x
a__plus(x,y): 3y + x
and(x,y): y + x
isNat(x): 0
isNatKind(x): 2x
mark(x): x
mark#(x): x
plus(x,y): 3y + x
s(x): x + 1
tt: 0

Standard Usable rules

a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))
mark(isNatKind(X))	→	a__isNatKind(X)	a__U22(tt)	→	tt
a__isNatKind(0)	→	tt	a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)
a__isNat(0)	→	tt	a__isNat(X)	→	isNat(X)
a__U21(tt, V1)	→	a__U22(a__isNat(V1))	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
a__U31(tt, N)	→	mark(N)	mark(U13(X))	→	a__U13(mark(X))
mark(U22(X))	→	a__U22(mark(X))	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__U13(tt)	→	tt
a__U12(X1, X2)	→	U12(X1, X2)	a__U22(X)	→	U22(X)
mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__U21(X1, X2)	→	U21(X1, X2)	mark(tt)	→	tt
mark(0)	→	0	a__plus(X1, X2)	→	plus(X1, X2)
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	a__and(X1, X2)	→	and(X1, X2)
a__and(tt, X)	→	mark(X)	a__U13(X)	→	U13(X)
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(isNat(X))	→	a__isNat(X)
a__U41(X1, X2, X3)	→	U41(X1, X2, X3)	mark(and(X1, X2))	→	a__and(mark(X1), X2)
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)
mark(s(X))	→	s(mark(X))	a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__U31(X1, X2)	→	U31(X1, X2)	mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__isNatKind(X)	→	isNatKind(X)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

a__isNatKind^#(s(V1))

→

a__isNatKind^#(V1)

Problem 17: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

mark^#(and(X1, X2))	→	mark^#(X1)	mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)
a__and^#(tt, X)	→	mark^#(X)	mark^#(isNatKind(X))	→	a__isNatKind^#(X)
a__isNatKind^#(plus(V1, V2))	→	a__and^#(a__isNatKind(V1), isNatKind(V2))	a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Function Precedence

U21 < isNat = U12 < U13 < s < a__U12 < a__U11 < isNatKind < U22 < 0 = U11 < a__isNatKind# < U31 < mark = mark# < a__and# = a__and = U41 = a__U41 = a__U22 = a__U21 = plus = a__plus = and = tt = a__isNat = a__U13 = a__U31 = a__isNatKind

Argument Filtering

a__and#: collapses to 2
a__and: 1 2
isNat: collapses to 1
U41: 2 3
a__U41: 2 3
a__U22: collapses to 1
a__U21: collapses to 2
U21: collapses to 2
U22: collapses to 1
plus: 1 2
isNatKind: collapses to 1
a__isNatKind#: collapses to 1
a__plus: 1 2
mark: collapses to 1
mark#: collapses to 1
and: 1 2
0: all arguments are removed from 0
s: collapses to 1
tt: all arguments are removed from tt
a__isNat: collapses to 1
a__U13: collapses to 1
a__U31: collapses to 2
U11: collapses to 3
a__U12: collapses to 2
U12: collapses to 2
a__U11: collapses to 3
U13: collapses to 1
U31: collapses to 2
a__isNatKind: collapses to 1

Status

a__and: lexicographic with permutation 1 → 1 2 → 2
U41: lexicographic with permutation 2 → 2 3 → 1
a__U41: lexicographic with permutation 2 → 2 3 → 1
plus: lexicographic with permutation 1 → 1 2 → 2
a__plus: lexicographic with permutation 1 → 1 2 → 2
and: lexicographic with permutation 1 → 1 2 → 2
0: multiset
tt: multiset

Usable Rules

a__U11(X1, X2, X3) → U11(X1, X2, X3)	a__U41(tt, M, N) → s(a__plus(mark(N), mark(M)))
mark(isNatKind(X)) → a__isNatKind(X)	a__U22(tt) → tt
a__isNatKind(0) → tt	a__U11(tt, V1, V2) → a__U12(a__isNat(V1), V2)
a__isNat(0) → tt	a__isNat(X) → isNat(X)
a__U21(tt, V1) → a__U22(a__isNat(V1))	mark(U12(X1, X2)) → a__U12(mark(X1), X2)
a__U31(tt, N) → mark(N)	mark(U13(X)) → a__U13(mark(X))
mark(U22(X)) → a__U22(mark(X))	a__U12(tt, V2) → a__U13(a__isNat(V2))
a__isNat(plus(V1, V2)) → a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__U13(tt) → tt
a__U12(X1, X2) → U12(X1, X2)	a__U22(X) → U22(X)
mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)	a__plus(N, s(M)) → a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__U21(X1, X2) → U21(X1, X2)	mark(tt) → tt
mark(0) → 0	a__plus(X1, X2) → plus(X1, X2)
mark(U21(X1, X2)) → a__U21(mark(X1), X2)	a__and(X1, X2) → and(X1, X2)
a__and(tt, X) → mark(X)	a__U13(X) → U13(X)
mark(U31(X1, X2)) → a__U31(mark(X1), X2)	mark(isNat(X)) → a__isNat(X)
a__U41(X1, X2, X3) → U41(X1, X2, X3)	mark(and(X1, X2)) → a__and(mark(X1), X2)
a__isNatKind(plus(V1, V2)) → a__and(a__isNatKind(V1), isNatKind(V2))	a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)
mark(s(X)) → s(mark(X))	a__plus(N, 0) → a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__U31(X1, X2) → U31(X1, X2)	mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)	a__isNatKind(s(V1)) → a__isNatKind(V1)
a__isNatKind(X) → isNatKind(X)

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

a__isNatKind^#(plus(V1, V2)) → a__and^#(a__isNatKind(V1), isNatKind(V2))

Problem 18: DependencyGraph

Dependency Pair Problem

Dependency Pairs

mark^#(and(X1, X2))	→	mark^#(X1)	mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)
a__and^#(tt, X)	→	mark^#(X)	mark^#(isNatKind(X))	→	a__isNatKind^#(X)
a__isNatKind^#(plus(V1, V2))	→	a__isNatKind^#(V1)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

The following SCCs where found

mark^#(and(X1, X2)) → mark^#(X1)	mark^#(and(X1, X2)) → a__and^#(mark(X1), X2)
a__and^#(tt, X) → mark^#(X)

a__isNatKind^#(plus(V1, V2)) → a__isNatKind^#(V1)

Problem 19: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

mark^#(and(X1, X2))	→	mark^#(X1)		mark^#(and(X1, X2))	→	a__and^#(mark(X1), X2)
a__and^#(tt, X)	→	mark^#(X)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Function Precedence

U11 = a__U11 < a__U21 < s < U13 < mark# < isNat < a__U22 = mark = 0 = tt = a__U12 < U12 < a__isNatKind < a__and# = a__and = U41 = a__U41 = U21 = U22 = plus = isNatKind = a__plus = and = a__isNat = a__U13 = a__U31 = U31

Argument Filtering

a__and#: 1 2
a__and: 1 2
isNat: collapses to 1
U41: 2 3
a__U41: 2 3
a__U22: collapses to 1
a__U21: collapses to 2
U21: collapses to 2
U22: collapses to 1
plus: 1 2
isNatKind: collapses to 1
a__plus: 1 2
mark: collapses to 1
mark#: collapses to 1
and: 1 2
0: all arguments are removed from 0
s: collapses to 1
tt: all arguments are removed from tt
a__isNat: collapses to 1
a__U13: collapses to 1
a__U31: collapses to 2
U11: collapses to 3
a__U12: collapses to 2
U12: collapses to 2
a__U11: collapses to 3
U13: collapses to 1
U31: collapses to 2
a__isNatKind: collapses to 1

Status

a__and#: lexicographic with permutation 1 → 2 2 → 1
a__and: lexicographic with permutation 1 → 2 2 → 1
U41: lexicographic with permutation 2 → 1 3 → 2
a__U41: lexicographic with permutation 2 → 1 3 → 2
plus: lexicographic with permutation 1 → 2 2 → 1
a__plus: lexicographic with permutation 1 → 2 2 → 1
and: lexicographic with permutation 1 → 2 2 → 1
0: multiset
tt: multiset

Usable Rules

a__U11(X1, X2, X3) → U11(X1, X2, X3)	a__U41(tt, M, N) → s(a__plus(mark(N), mark(M)))
mark(isNatKind(X)) → a__isNatKind(X)	a__U22(tt) → tt
a__isNatKind(0) → tt	a__U11(tt, V1, V2) → a__U12(a__isNat(V1), V2)
a__isNat(0) → tt	a__isNat(X) → isNat(X)
a__U21(tt, V1) → a__U22(a__isNat(V1))	mark(U12(X1, X2)) → a__U12(mark(X1), X2)
a__U31(tt, N) → mark(N)	mark(U13(X)) → a__U13(mark(X))
mark(U22(X)) → a__U22(mark(X))	a__U12(tt, V2) → a__U13(a__isNat(V2))
a__isNat(plus(V1, V2)) → a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__U22(X) → U22(X)
a__U12(X1, X2) → U12(X1, X2)	a__U13(tt) → tt
mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)	a__plus(N, s(M)) → a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__U21(X1, X2) → U21(X1, X2)	mark(tt) → tt
mark(0) → 0	a__plus(X1, X2) → plus(X1, X2)
a__and(X1, X2) → and(X1, X2)	mark(U21(X1, X2)) → a__U21(mark(X1), X2)
a__U13(X) → U13(X)	a__and(tt, X) → mark(X)
mark(U31(X1, X2)) → a__U31(mark(X1), X2)	mark(isNat(X)) → a__isNat(X)
a__U41(X1, X2, X3) → U41(X1, X2, X3)	mark(and(X1, X2)) → a__and(mark(X1), X2)
a__isNatKind(plus(V1, V2)) → a__and(a__isNatKind(V1), isNatKind(V2))	a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)
mark(s(X)) → s(mark(X))	a__plus(N, 0) → a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__U31(X1, X2) → U31(X1, X2)	mark(plus(X1, X2)) → a__plus(mark(X1), mark(X2))
a__isNatKind(s(V1)) → a__isNatKind(V1)	a__isNatKind(X) → isNatKind(X)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

a__and^#(tt, X) → mark^#(X)

Problem 21: DependencyGraph

Dependency Pair Problem

Dependency Pairs

mark^#(and(X1, X2))

→

mark^#(X1)

mark^#(and(X1, X2))

→

a__and^#(mark(X1), X2)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

The following SCCs where found

mark^#(and(X1, X2)) → mark^#(X1)

Problem 22: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

mark^#(and(X1, X2))

→

mark^#(X1)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Function Precedence

a__and = isNat = U41 = a__U41 = a__U22 = a__U21 = U21 = U22 = plus = isNatKind = a__plus = mark = mark# = and = 0 = s = tt = a__isNat = a__U13 = a__U31 = U11 = U12 = a__U12 = a__U11 = U13 = U31 = a__isNatKind

Argument Filtering

a__and: collapses to 1
isNat: all arguments are removed from isNat
U41: 1 2
a__U41: all arguments are removed from a__U41
a__U22: all arguments are removed from a__U22
a__U21: all arguments are removed from a__U21
U21: 1 2
U22: all arguments are removed from U22
plus: all arguments are removed from plus
isNatKind: all arguments are removed from isNatKind
a__plus: all arguments are removed from a__plus
mark: all arguments are removed from mark
mark#: 1
and: 1
0: all arguments are removed from 0
s: all arguments are removed from s
tt: all arguments are removed from tt
a__isNat: all arguments are removed from a__isNat
a__U13: all arguments are removed from a__U13
a__U31: all arguments are removed from a__U31
U11: all arguments are removed from U11
U12: all arguments are removed from U12
a__U12: all arguments are removed from a__U12
a__U11: 2 3
U13: all arguments are removed from U13
U31: all arguments are removed from U31
a__isNatKind: all arguments are removed from a__isNatKind

Status

isNat: multiset
U41: lexicographic with permutation 1 → 2 2 → 1
a__U41: multiset
a__U22: multiset
a__U21: multiset
U21: lexicographic with permutation 1 → 2 2 → 1
U22: multiset
plus: multiset
isNatKind: multiset
a__plus: multiset
mark: multiset
mark#: multiset
and: multiset
0: multiset
s: multiset
tt: multiset
a__isNat: multiset
a__U13: multiset
a__U31: multiset
U11: multiset
U12: multiset
a__U12: multiset
a__U11: lexicographic with permutation 2 → 1 3 → 2
U13: multiset
U31: multiset
a__isNatKind: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

mark^#(and(X1, X2)) → mark^#(X1)

Problem 20: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

a__isNatKind^#(plus(V1, V2))

→

a__isNatKind^#(V1)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Function Precedence

a__and = isNat = U41 = a__U41 = a__U22 = a__U21 = U21 = U22 = plus = isNatKind = a__isNatKind# = a__plus = mark = and = 0 = s = tt = a__isNat = a__U13 = a__U31 = U11 = U12 = a__U12 = a__U11 = U13 = U31 = a__isNatKind

Argument Filtering

a__and: 1
isNat: all arguments are removed from isNat
U41: 2
a__U41: 1 2 3
a__U22: all arguments are removed from a__U22
a__U21: all arguments are removed from a__U21
U21: collapses to 2
U22: 1
plus: 1 2
isNatKind: 1
a__isNatKind#: 1
a__plus: all arguments are removed from a__plus
mark: all arguments are removed from mark
and: all arguments are removed from and
0: all arguments are removed from 0
s: all arguments are removed from s
tt: all arguments are removed from tt
a__isNat: all arguments are removed from a__isNat
a__U13: all arguments are removed from a__U13
a__U31: all arguments are removed from a__U31
U11: all arguments are removed from U11
U12: all arguments are removed from U12
a__U12: collapses to 1
a__U11: all arguments are removed from a__U11
U13: all arguments are removed from U13
U31: 1 2
a__isNatKind: collapses to 1

Status

a__and: lexicographic with permutation 1 → 1
isNat: multiset
U41: lexicographic with permutation 2 → 1
a__U41: lexicographic with permutation 1 → 2 2 → 3 3 → 1
a__U22: multiset
a__U21: multiset
U22: lexicographic with permutation 1 → 1
plus: multiset
isNatKind: lexicographic with permutation 1 → 1
a__isNatKind#: lexicographic with permutation 1 → 1
a__plus: multiset
mark: multiset
and: multiset
0: multiset
s: multiset
tt: multiset
a__isNat: multiset
a__U13: multiset
a__U31: multiset
U11: multiset
U12: multiset
a__U11: multiset
U13: multiset
U31: lexicographic with permutation 1 → 2 2 → 1

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

a__isNatKind^#(plus(V1, V2)) → a__isNatKind^#(V1)

Problem 6: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

a__U41^#(tt, M, N)

→

a__plus^#(mark(N), mark(M))

a__plus^#(N, s(M))

→

a__U41^#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

Original Signature

Strategy

Polynomial Interpretation

0: 2
U11(x,y,z): z
U12(x,y): y
U13(x): x
U21(x,y): y + x
U22(x): x
U31(x,y): y
U41(x,y,z): 2z + y + x
a__U11(x,y,z): z
a__U12(x,y): y
a__U13(x): x
a__U21(x,y): y + x
a__U22(x): x
a__U31(x,y): y
a__U41(x,y,z): 2z + y + x
a__U41#(x,y,z): y
a__and(x,y): y
a__isNat(x): x
a__isNatKind(x): 2
a__plus(x,y): y + 2x
a__plus#(x,y): y
and(x,y): y
isNat(x): x
isNatKind(x): 2
mark(x): x
plus(x,y): y + 2x
s(x): x + 2
tt: 2

Standard Usable rules

a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))
mark(isNatKind(X))	→	a__isNatKind(X)	a__U22(tt)	→	tt
a__isNatKind(0)	→	tt	a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)
a__isNat(0)	→	tt	a__isNat(X)	→	isNat(X)
a__U21(tt, V1)	→	a__U22(a__isNat(V1))	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
a__U31(tt, N)	→	mark(N)	mark(U13(X))	→	a__U13(mark(X))
mark(U22(X))	→	a__U22(mark(X))	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)	a__U13(tt)	→	tt
a__U12(X1, X2)	→	U12(X1, X2)	a__U22(X)	→	U22(X)
mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
a__U21(X1, X2)	→	U21(X1, X2)	mark(tt)	→	tt
mark(0)	→	0	a__plus(X1, X2)	→	plus(X1, X2)
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	a__and(X1, X2)	→	and(X1, X2)
a__U13(X)	→	U13(X)	a__and(tt, X)	→	mark(X)
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(isNat(X))	→	a__isNat(X)
a__U41(X1, X2, X3)	→	U41(X1, X2, X3)	mark(and(X1, X2))	→	a__and(mark(X1), X2)
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)
mark(s(X))	→	s(mark(X))	a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)
a__U31(X1, X2)	→	U31(X1, X2)	mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))
a__isNatKind(s(V1))	→	a__isNatKind(V1)	a__isNatKind(X)	→	isNatKind(X)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

a__plus^#(N, s(M))

→

a__U41^#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)

Problem 8: DependencyGraph

Dependency Pair Problem

Dependency Pairs

a__U41^#(tt, M, N)

→

a__plus^#(mark(N), mark(M))

Rewrite Rules

a__U11(tt, V1, V2)	→	a__U12(a__isNat(V1), V2)	a__U12(tt, V2)	→	a__U13(a__isNat(V2))
a__U13(tt)	→	tt	a__U21(tt, V1)	→	a__U22(a__isNat(V1))
a__U22(tt)	→	tt	a__U31(tt, N)	→	mark(N)
a__U41(tt, M, N)	→	s(a__plus(mark(N), mark(M)))	a__and(tt, X)	→	mark(X)
a__isNat(0)	→	tt	a__isNat(plus(V1, V2))	→	a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1), V1)	a__isNatKind(0)	→	tt
a__isNatKind(plus(V1, V2))	→	a__and(a__isNatKind(V1), isNatKind(V2))	a__isNatKind(s(V1))	→	a__isNatKind(V1)
a__plus(N, 0)	→	a__U31(a__and(a__isNat(N), isNatKind(N)), N)	a__plus(N, s(M))	→	a__U41(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)
mark(U11(X1, X2, X3))	→	a__U11(mark(X1), X2, X3)	mark(U12(X1, X2))	→	a__U12(mark(X1), X2)
mark(isNat(X))	→	a__isNat(X)	mark(U13(X))	→	a__U13(mark(X))
mark(U21(X1, X2))	→	a__U21(mark(X1), X2)	mark(U22(X))	→	a__U22(mark(X))
mark(U31(X1, X2))	→	a__U31(mark(X1), X2)	mark(U41(X1, X2, X3))	→	a__U41(mark(X1), X2, X3)
mark(plus(X1, X2))	→	a__plus(mark(X1), mark(X2))	mark(and(X1, X2))	→	a__and(mark(X1), X2)
mark(isNatKind(X))	→	a__isNatKind(X)	mark(tt)	→	tt
mark(s(X))	→	s(mark(X))	mark(0)	→	0
a__U11(X1, X2, X3)	→	U11(X1, X2, X3)	a__U12(X1, X2)	→	U12(X1, X2)
a__isNat(X)	→	isNat(X)	a__U13(X)	→	U13(X)
a__U21(X1, X2)	→	U21(X1, X2)	a__U22(X)	→	U22(X)
a__U31(X1, X2)	→	U31(X1, X2)	a__U41(X1, X2, X3)	→	U41(X1, X2, X3)
a__plus(X1, X2)	→	plus(X1, X2)	a__and(X1, X2)	→	and(X1, X2)
a__isNatKind(X)	→	isNatKind(X)

The following DP Processors were used

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

The following SCCs where found

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

Polynomial Interpretation

Standard Usable rules

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

Polynomial Interpretation

Standard Usable rules

Problem 4: DependencyGraph

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

The following SCCs where found

Problem 5: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

Polynomial Interpretation

Standard Usable rules

Problem 7: DependencyGraph

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

The following SCCs where found

Problem 9: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

Polynomial Interpretation

Standard Usable rules

Problem 10: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

Polynomial Interpretation

Standard Usable rules

Problem 11: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

Polynomial Interpretation

Standard Usable rules

Problem 12: DependencyGraph

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

The following SCCs where found

Problem 13: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs