Open Dependency Pair Problem 2

Dependency Pairs

take^#(s(M), cons(N, IL))	→	isNatIList^#(activate(IL))	isNatIList^#(n__cons(V1, V2))	→	activate^#(V2)
and^#(tt, X)	→	activate^#(X)	activate^#(n__isNatIList(X))	→	isNatIList^#(X)
activate^#(n__and(X1, X2))	→	activate^#(X1)	isNatList^#(n__cons(V1, V2))	→	and^#(isNat(activate(V1)), n__isNatList(activate(V2)))
activate^#(n__length(X))	→	activate^#(X)	activate^#(n__and(X1, X2))	→	and^#(activate(X1), X2)
activate^#(n__s(X))	→	activate^#(X)	isNatList^#(n__take(V1, V2))	→	activate^#(V1)
isNatIList^#(n__cons(V1, V2))	→	and^#(isNat(activate(V1)), n__isNatIList(activate(V2)))	length^#(cons(N, L))	→	and^#(isNatList(activate(L)), n__isNat(N))
isNatList^#(n__cons(V1, V2))	→	isNat^#(activate(V1))	activate^#(n__take(X1, X2))	→	take^#(activate(X1), activate(X2))
U31^#(tt, IL, M, N)	→	activate^#(N)	take^#(s(M), cons(N, IL))	→	U31^#(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
activate^#(n__cons(X1, X2))	→	activate^#(X1)	U31^#(tt, IL, M, N)	→	activate^#(M)
take^#(s(M), cons(N, IL))	→	and^#(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N)))	U31^#(tt, IL, M, N)	→	activate^#(IL)
activate^#(n__isNat(X))	→	isNat^#(X)	isNatIList^#(V)	→	activate^#(V)
activate^#(n__take(X1, X2))	→	activate^#(X2)	isNat^#(n__length(V1))	→	activate^#(V1)
isNat^#(n__s(V1))	→	activate^#(V1)	isNatIList^#(V)	→	isNatList^#(activate(V))
isNatList^#(n__take(V1, V2))	→	and^#(isNat(activate(V1)), n__isNatIList(activate(V2)))	isNatList^#(n__cons(V1, V2))	→	activate^#(V2)
isNatList^#(n__take(V1, V2))	→	isNat^#(activate(V1))	U11^#(tt, L)	→	activate^#(L)
activate^#(n__length(X))	→	length^#(activate(X))	activate^#(n__isNatList(X))	→	isNatList^#(X)
length^#(cons(N, L))	→	isNatList^#(activate(L))	isNatList^#(n__take(V1, V2))	→	activate^#(V2)
isNat^#(n__length(V1))	→	isNatList^#(activate(V1))	activate^#(n__take(X1, X2))	→	activate^#(X1)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	isNatList^#(n__cons(V1, V2))	→	activate^#(V1)
take^#(s(M), cons(N, IL))	→	activate^#(IL)	isNatIList^#(n__cons(V1, V2))	→	isNat^#(activate(V1))
take^#(0, IL)	→	isNatIList^#(IL)	U11^#(tt, L)	→	length^#(activate(L))
isNatIList^#(n__cons(V1, V2))	→	activate^#(V1)	length^#(cons(N, L))	→	U11^#(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length^#(cons(N, L))	→	activate^#(L)

Rewrite Rules

zeros	→	cons(0, n__zeros)	U11(tt, L)	→	s(length(activate(L)))
U21(tt)	→	nil	U31(tt, IL, M, N)	→	cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X)	→	activate(X)	isNat(n__0)	→	tt
isNat(n__length(V1))	→	isNatList(activate(V1))	isNat(n__s(V1))	→	isNat(activate(V1))
isNatIList(V)	→	isNatList(activate(V))	isNatIList(n__zeros)	→	tt
isNatIList(n__cons(V1, V2))	→	and(isNat(activate(V1)), n__isNatIList(activate(V2)))	isNatList(n__nil)	→	tt
isNatList(n__cons(V1, V2))	→	and(isNat(activate(V1)), n__isNatList(activate(V2)))	isNatList(n__take(V1, V2))	→	and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil)	→	0	length(cons(N, L))	→	U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL)	→	U21(isNatIList(IL))	take(s(M), cons(N, IL))	→	U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
zeros	→	n__zeros	take(X1, X2)	→	n__take(X1, X2)
0	→	n__0	length(X)	→	n__length(X)
s(X)	→	n__s(X)	cons(X1, X2)	→	n__cons(X1, X2)
isNatIList(X)	→	n__isNatIList(X)	nil	→	n__nil
isNatList(X)	→	n__isNatList(X)	isNat(X)	→	n__isNat(X)
and(X1, X2)	→	n__and(X1, X2)	activate(n__zeros)	→	zeros
activate(n__take(X1, X2))	→	take(activate(X1), activate(X2))	activate(n__0)	→	0
activate(n__length(X))	→	length(activate(X))	activate(n__s(X))	→	s(activate(X))
activate(n__cons(X1, X2))	→	cons(activate(X1), X2)	activate(n__isNatIList(X))	→	isNatIList(X)
activate(n__nil)	→	nil	activate(n__isNatList(X))	→	isNatList(X)
activate(n__isNat(X))	→	isNat(X)	activate(n__and(X1, X2))	→	and(activate(X1), X2)
activate(X)	→	X

Original Signature

Termination of terms over the following signature is verified: n__isNatIList, activate, isNat, n__s, n__0, length, n__nil, n__zeros, U21, cons, isNatIList, n__length, n__take, n__isNat, and, n__isNatList, n__and, n__cons, 0, s, isNatList, tt, zeros, take, U11, U31, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

take^#(s(M), cons(N, IL))	→	isNatIList^#(activate(IL))	and^#(tt, X)	→	activate^#(X)
isNatList^#(n__cons(V1, V2))	→	and^#(isNat(activate(V1)), n__isNatList(activate(V2)))	activate^#(n__and(X1, X2))	→	and^#(activate(X1), X2)
zeros^#	→	0^#	isNatList^#(n__take(V1, V2))	→	activate^#(V1)
isNatList^#(n__cons(V1, V2))	→	isNat^#(activate(V1))	activate^#(n__take(X1, X2))	→	take^#(activate(X1), activate(X2))
activate^#(n__cons(X1, X2))	→	cons^#(activate(X1), X2)	U31^#(tt, IL, M, N)	→	activate^#(N)
activate^#(n__cons(X1, X2))	→	activate^#(X1)	take^#(s(M), cons(N, IL))	→	U31^#(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
U31^#(tt, IL, M, N)	→	activate^#(M)	take^#(s(M), cons(N, IL))	→	and^#(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N)))
U31^#(tt, IL, M, N)	→	activate^#(IL)	activate^#(n__isNat(X))	→	isNat^#(X)
isNat^#(n__length(V1))	→	activate^#(V1)	isNat^#(n__s(V1))	→	activate^#(V1)
length^#(nil)	→	0^#	isNatList^#(n__take(V1, V2))	→	and^#(isNat(activate(V1)), n__isNatIList(activate(V2)))
U31^#(tt, IL, M, N)	→	cons^#(activate(N), n__take(activate(M), activate(IL)))	isNatList^#(n__cons(V1, V2))	→	activate^#(V2)
isNatList^#(n__take(V1, V2))	→	isNat^#(activate(V1))	U11^#(tt, L)	→	activate^#(L)
activate^#(n__length(X))	→	length^#(activate(X))	length^#(cons(N, L))	→	isNatList^#(activate(L))
isNat^#(n__length(V1))	→	isNatList^#(activate(V1))	isNatList^#(n__take(V1, V2))	→	activate^#(V2)
activate^#(n__0)	→	0^#	isNatIList^#(n__cons(V1, V2))	→	isNat^#(activate(V1))
take^#(s(M), cons(N, IL))	→	activate^#(IL)	U11^#(tt, L)	→	length^#(activate(L))
length^#(cons(N, L))	→	U11^#(and(isNatList(activate(L)), n__isNat(N)), activate(L))	isNatIList^#(n__cons(V1, V2))	→	activate^#(V2)
activate^#(n__zeros)	→	zeros^#	activate^#(n__isNatIList(X))	→	isNatIList^#(X)
activate^#(n__and(X1, X2))	→	activate^#(X1)	activate^#(n__length(X))	→	activate^#(X)
activate^#(n__s(X))	→	activate^#(X)	isNatIList^#(n__cons(V1, V2))	→	and^#(isNat(activate(V1)), n__isNatIList(activate(V2)))
length^#(cons(N, L))	→	and^#(isNatList(activate(L)), n__isNat(N))	take^#(0, IL)	→	U21^#(isNatIList(IL))
U21^#(tt)	→	nil^#	U11^#(tt, L)	→	s^#(length(activate(L)))
isNatIList^#(V)	→	activate^#(V)	activate^#(n__take(X1, X2))	→	activate^#(X2)
isNatIList^#(V)	→	isNatList^#(activate(V))	zeros^#	→	cons^#(0, n__zeros)
activate^#(n__isNatList(X))	→	isNatList^#(X)	activate^#(n__nil)	→	nil^#
activate^#(n__take(X1, X2))	→	activate^#(X1)	isNat^#(n__s(V1))	→	isNat^#(activate(V1))
isNatList^#(n__cons(V1, V2))	→	activate^#(V1)	activate^#(n__s(X))	→	s^#(activate(X))
take^#(0, IL)	→	isNatIList^#(IL)	isNatIList^#(n__cons(V1, V2))	→	activate^#(V1)
length^#(cons(N, L))	→	activate^#(L)

Rewrite Rules

zeros	→	cons(0, n__zeros)	U11(tt, L)	→	s(length(activate(L)))
U21(tt)	→	nil	U31(tt, IL, M, N)	→	cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X)	→	activate(X)	isNat(n__0)	→	tt
isNat(n__length(V1))	→	isNatList(activate(V1))	isNat(n__s(V1))	→	isNat(activate(V1))
isNatIList(V)	→	isNatList(activate(V))	isNatIList(n__zeros)	→	tt
isNatIList(n__cons(V1, V2))	→	and(isNat(activate(V1)), n__isNatIList(activate(V2)))	isNatList(n__nil)	→	tt
isNatList(n__cons(V1, V2))	→	and(isNat(activate(V1)), n__isNatList(activate(V2)))	isNatList(n__take(V1, V2))	→	and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil)	→	0	length(cons(N, L))	→	U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL)	→	U21(isNatIList(IL))	take(s(M), cons(N, IL))	→	U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
zeros	→	n__zeros	take(X1, X2)	→	n__take(X1, X2)
0	→	n__0	length(X)	→	n__length(X)
s(X)	→	n__s(X)	cons(X1, X2)	→	n__cons(X1, X2)
isNatIList(X)	→	n__isNatIList(X)	nil	→	n__nil
isNatList(X)	→	n__isNatList(X)	isNat(X)	→	n__isNat(X)
and(X1, X2)	→	n__and(X1, X2)	activate(n__zeros)	→	zeros
activate(n__take(X1, X2))	→	take(activate(X1), activate(X2))	activate(n__0)	→	0
activate(n__length(X))	→	length(activate(X))	activate(n__s(X))	→	s(activate(X))
activate(n__cons(X1, X2))	→	cons(activate(X1), X2)	activate(n__isNatIList(X))	→	isNatIList(X)
activate(n__nil)	→	nil	activate(n__isNatList(X))	→	isNatList(X)
activate(n__isNat(X))	→	isNat(X)	activate(n__and(X1, X2))	→	and(activate(X1), X2)
activate(X)	→	X

Original Signature

Termination of terms over the following signature is verified: n__isNatIList, n__s, isNat, activate, n__0, length, n__nil, n__zeros, U21, cons, isNatIList, n__length, n__take, n__isNat, and, n__isNatList, n__and, n__cons, 0, s, isNatList, tt, zeros, take, U11, U31, nil

Strategy

The following SCCs where found

take^#(s(M), cons(N, IL)) → isNatIList^#(activate(IL))	and^#(tt, X) → activate^#(X)
isNatIList^#(n__cons(V1, V2)) → activate^#(V2)	activate^#(n__isNatIList(X)) → isNatIList^#(X)
activate^#(n__and(X1, X2)) → activate^#(X1)	activate^#(n__length(X)) → activate^#(X)
isNatList^#(n__cons(V1, V2)) → and^#(isNat(activate(V1)), n__isNatList(activate(V2)))	activate^#(n__and(X1, X2)) → and^#(activate(X1), X2)
activate^#(n__s(X)) → activate^#(X)	isNatIList^#(n__cons(V1, V2)) → and^#(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList^#(n__take(V1, V2)) → activate^#(V1)	length^#(cons(N, L)) → and^#(isNatList(activate(L)), n__isNat(N))
isNatList^#(n__cons(V1, V2)) → isNat^#(activate(V1))	activate^#(n__take(X1, X2)) → take^#(activate(X1), activate(X2))
U31^#(tt, IL, M, N) → activate^#(N)	activate^#(n__cons(X1, X2)) → activate^#(X1)
take^#(s(M), cons(N, IL)) → U31^#(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)	U31^#(tt, IL, M, N) → activate^#(M)
U31^#(tt, IL, M, N) → activate^#(IL)	take^#(s(M), cons(N, IL)) → and^#(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N)))
activate^#(n__isNat(X)) → isNat^#(X)	activate^#(n__take(X1, X2)) → activate^#(X2)
isNatIList^#(V) → activate^#(V)	isNat^#(n__s(V1)) → activate^#(V1)
isNat^#(n__length(V1)) → activate^#(V1)	isNatList^#(n__take(V1, V2)) → and^#(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatIList^#(V) → isNatList^#(activate(V))	isNatList^#(n__cons(V1, V2)) → activate^#(V2)
isNatList^#(n__take(V1, V2)) → isNat^#(activate(V1))	U11^#(tt, L) → activate^#(L)
activate^#(n__length(X)) → length^#(activate(X))	activate^#(n__isNatList(X)) → isNatList^#(X)
length^#(cons(N, L)) → isNatList^#(activate(L))	isNat^#(n__length(V1)) → isNatList^#(activate(V1))
isNatList^#(n__take(V1, V2)) → activate^#(V2)	activate^#(n__take(X1, X2)) → activate^#(X1)
isNat^#(n__s(V1)) → isNat^#(activate(V1))	isNatList^#(n__cons(V1, V2)) → activate^#(V1)
isNatIList^#(n__cons(V1, V2)) → isNat^#(activate(V1))	take^#(s(M), cons(N, IL)) → activate^#(IL)
take^#(0, IL) → isNatIList^#(IL)	isNatIList^#(n__cons(V1, V2)) → activate^#(V1)
U11^#(tt, L) → length^#(activate(L))	length^#(cons(N, L)) → U11^#(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length^#(cons(N, L)) → activate^#(L)

The following DP Processors were used

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

Rewrite Rules

Original Signature

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

The following SCCs where found