Open Dependency Pair Problem 2

Dependency Pairs

take^#(s(M), cons(N, IL))	→	isNatIList^#(activate(IL))	isNatList^#(n__take(N, IL))	→	isNat^#(activate(N))
length^#(cons(N, L))	→	isNat^#(N)	isNatList^#(n__take(N, IL))	→	activate^#(IL)
uLength^#(tt, L)	→	length^#(activate(L))	isNatList^#(n__take(N, IL))	→	isNatIList^#(activate(IL))
uTake2^#(tt, M, N, IL)	→	activate^#(IL)	isNat^#(n__length(L))	→	isNatList^#(activate(L))
isNatList^#(n__cons(N, L))	→	isNatList^#(activate(L))	uTake2^#(tt, M, N, IL)	→	activate^#(M)
isNatIList^#(IL)	→	activate^#(IL)	isNatIList^#(n__cons(N, IL))	→	isNat^#(activate(N))
isNat^#(n__s(N))	→	isNat^#(activate(N))	take^#(s(M), cons(N, IL))	→	isNat^#(N)
isNatList^#(n__cons(N, L))	→	activate^#(L)	isNat^#(n__length(L))	→	activate^#(L)
length^#(cons(N, L))	→	uLength^#(and(isNat(N), isNatList(activate(L))), activate(L))	isNatList^#(n__take(N, IL))	→	activate^#(N)
isNatIList^#(n__cons(N, IL))	→	isNatIList^#(activate(IL))	isNatList^#(n__cons(N, L))	→	activate^#(N)
isNatIList^#(IL)	→	isNatList^#(activate(IL))	isNat^#(n__s(N))	→	activate^#(N)
uLength^#(tt, L)	→	activate^#(L)	take^#(s(M), cons(N, IL))	→	uTake2^#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
isNatIList^#(n__cons(N, IL))	→	activate^#(IL)	uTake2^#(tt, M, N, IL)	→	activate^#(N)
length^#(cons(N, L))	→	isNatList^#(activate(L))	activate^#(n__length(X))	→	length^#(X)
isNatList^#(n__cons(N, L))	→	isNat^#(activate(N))	isNatIList^#(n__cons(N, IL))	→	activate^#(N)
activate^#(n__take(X1, X2))	→	take^#(X1, X2)	take^#(s(M), cons(N, IL))	→	activate^#(IL)
take^#(0, IL)	→	isNatIList^#(IL)	take^#(s(M), cons(N, IL))	→	isNat^#(M)
length^#(cons(N, L))	→	activate^#(L)

Rewrite Rules

and(tt, T)	→	T	isNatIList(IL)	→	isNatList(activate(IL))
isNat(n__0)	→	tt	isNat(n__s(N))	→	isNat(activate(N))
isNat(n__length(L))	→	isNatList(activate(L))	isNatIList(n__zeros)	→	tt
isNatIList(n__cons(N, IL))	→	and(isNat(activate(N)), isNatIList(activate(IL)))	isNatList(n__nil)	→	tt
isNatList(n__cons(N, L))	→	and(isNat(activate(N)), isNatList(activate(L)))	isNatList(n__take(N, IL))	→	and(isNat(activate(N)), isNatIList(activate(IL)))
zeros	→	cons(0, n__zeros)	take(0, IL)	→	uTake1(isNatIList(IL))
uTake1(tt)	→	nil	take(s(M), cons(N, IL))	→	uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
uTake2(tt, M, N, IL)	→	cons(activate(N), n__take(activate(M), activate(IL)))	length(cons(N, L))	→	uLength(and(isNat(N), isNatList(activate(L))), activate(L))
uLength(tt, L)	→	s(length(activate(L)))	0	→	n__0
s(X)	→	n__s(X)	length(X)	→	n__length(X)
zeros	→	n__zeros	cons(X1, X2)	→	n__cons(X1, X2)
nil	→	n__nil	take(X1, X2)	→	n__take(X1, X2)
activate(n__0)	→	0	activate(n__s(X))	→	s(X)
activate(n__length(X))	→	length(X)	activate(n__zeros)	→	zeros
activate(n__cons(X1, X2))	→	cons(X1, X2)	activate(n__nil)	→	nil
activate(n__take(X1, X2))	→	take(X1, X2)	activate(X)	→	X

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, n__length, n__take, and, uTake1, activate, isNat, n__s, n__cons, uTake2, 0, n__0, s, isNatList, zeros, tt, take, length, n__nil, n__zeros, nil, cons

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

take^#(s(M), cons(N, IL))	→	isNatIList^#(activate(IL))	isNatList^#(n__take(N, IL))	→	isNat^#(activate(N))
zeros^#	→	0^#	uLength^#(tt, L)	→	length^#(activate(L))
uTake1^#(tt)	→	nil^#	uTake2^#(tt, M, N, IL)	→	activate^#(IL)
uTake2^#(tt, M, N, IL)	→	activate^#(M)	take^#(s(M), cons(N, IL))	→	and^#(isNat(N), isNatIList(activate(IL)))
isNat^#(n__s(N))	→	isNat^#(activate(N))	isNatList^#(n__cons(N, L))	→	activate^#(L)
isNat^#(n__length(L))	→	activate^#(L)	isNatList^#(n__take(N, IL))	→	activate^#(N)
uLength^#(tt, L)	→	s^#(length(activate(L)))	isNatList^#(n__cons(N, L))	→	activate^#(N)
isNatIList^#(n__cons(N, IL))	→	and^#(isNat(activate(N)), isNatIList(activate(IL)))	isNatIList^#(IL)	→	isNatList^#(activate(IL))
uLength^#(tt, L)	→	activate^#(L)	isNat^#(n__s(N))	→	activate^#(N)
take^#(s(M), cons(N, IL))	→	uTake2^#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))	length^#(cons(N, L))	→	isNatList^#(activate(L))
uTake2^#(tt, M, N, IL)	→	activate^#(N)	isNatIList^#(n__cons(N, IL))	→	activate^#(N)
activate^#(n__0)	→	0^#	take^#(s(M), cons(N, IL))	→	activate^#(IL)
activate^#(n__zeros)	→	zeros^#	length^#(cons(N, L))	→	isNat^#(N)
isNatList^#(n__take(N, IL))	→	activate^#(IL)	take^#(s(M), cons(N, IL))	→	and^#(isNat(M), and(isNat(N), isNatIList(activate(IL))))
isNatList^#(n__take(N, IL))	→	isNatIList^#(activate(IL))	uTake2^#(tt, M, N, IL)	→	cons^#(activate(N), n__take(activate(M), activate(IL)))
isNat^#(n__length(L))	→	isNatList^#(activate(L))	isNatList^#(n__cons(N, L))	→	isNatList^#(activate(L))
isNatIList^#(IL)	→	activate^#(IL)	isNatIList^#(n__cons(N, IL))	→	isNat^#(activate(N))
take^#(s(M), cons(N, IL))	→	isNat^#(N)	activate^#(n__cons(X1, X2))	→	cons^#(X1, X2)
length^#(cons(N, L))	→	uLength^#(and(isNat(N), isNatList(activate(L))), activate(L))	zeros^#	→	cons^#(0, n__zeros)
length^#(cons(N, L))	→	and^#(isNat(N), isNatList(activate(L)))	isNatIList^#(n__cons(N, IL))	→	isNatIList^#(activate(IL))
take^#(0, IL)	→	uTake1^#(isNatIList(IL))	isNatList^#(n__cons(N, L))	→	and^#(isNat(activate(N)), isNatList(activate(L)))
isNatIList^#(n__cons(N, IL))	→	activate^#(IL)	activate^#(n__s(X))	→	s^#(X)
activate^#(n__nil)	→	nil^#	activate^#(n__length(X))	→	length^#(X)
isNatList^#(n__cons(N, L))	→	isNat^#(activate(N))	activate^#(n__take(X1, X2))	→	take^#(X1, X2)
isNatList^#(n__take(N, IL))	→	and^#(isNat(activate(N)), isNatIList(activate(IL)))	take^#(0, IL)	→	isNatIList^#(IL)
take^#(s(M), cons(N, IL))	→	isNat^#(M)	length^#(cons(N, L))	→	activate^#(L)

Rewrite Rules

and(tt, T)	→	T	isNatIList(IL)	→	isNatList(activate(IL))
isNat(n__0)	→	tt	isNat(n__s(N))	→	isNat(activate(N))
isNat(n__length(L))	→	isNatList(activate(L))	isNatIList(n__zeros)	→	tt
isNatIList(n__cons(N, IL))	→	and(isNat(activate(N)), isNatIList(activate(IL)))	isNatList(n__nil)	→	tt
isNatList(n__cons(N, L))	→	and(isNat(activate(N)), isNatList(activate(L)))	isNatList(n__take(N, IL))	→	and(isNat(activate(N)), isNatIList(activate(IL)))
zeros	→	cons(0, n__zeros)	take(0, IL)	→	uTake1(isNatIList(IL))
uTake1(tt)	→	nil	take(s(M), cons(N, IL))	→	uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
uTake2(tt, M, N, IL)	→	cons(activate(N), n__take(activate(M), activate(IL)))	length(cons(N, L))	→	uLength(and(isNat(N), isNatList(activate(L))), activate(L))
uLength(tt, L)	→	s(length(activate(L)))	0	→	n__0
s(X)	→	n__s(X)	length(X)	→	n__length(X)
zeros	→	n__zeros	cons(X1, X2)	→	n__cons(X1, X2)
nil	→	n__nil	take(X1, X2)	→	n__take(X1, X2)
activate(n__0)	→	0	activate(n__s(X))	→	s(X)
activate(n__length(X))	→	length(X)	activate(n__zeros)	→	zeros
activate(n__cons(X1, X2))	→	cons(X1, X2)	activate(n__nil)	→	nil
activate(n__take(X1, X2))	→	take(X1, X2)	activate(X)	→	X

Original Signature

Termination of terms over the following signature is verified: isNatIList, uLength, n__length, n__take, and, uTake1, activate, isNat, n__s, n__cons, uTake2, 0, n__0, isNatList, s, tt, zeros, take, length, n__nil, n__zeros, cons, nil

Strategy

The following SCCs where found

take^#(s(M), cons(N, IL)) → isNatIList^#(activate(IL))	isNatList^#(n__take(N, IL)) → isNat^#(activate(N))
length^#(cons(N, L)) → isNat^#(N)	isNatList^#(n__take(N, IL)) → activate^#(IL)
uLength^#(tt, L) → length^#(activate(L))	isNatList^#(n__take(N, IL)) → isNatIList^#(activate(IL))
uTake2^#(tt, M, N, IL) → activate^#(IL)	isNat^#(n__length(L)) → isNatList^#(activate(L))
isNatList^#(n__cons(N, L)) → isNatList^#(activate(L))	uTake2^#(tt, M, N, IL) → activate^#(M)
isNatIList^#(IL) → activate^#(IL)	isNatIList^#(n__cons(N, IL)) → isNat^#(activate(N))
isNat^#(n__s(N)) → isNat^#(activate(N))	take^#(s(M), cons(N, IL)) → isNat^#(N)
isNatList^#(n__cons(N, L)) → activate^#(L)	isNat^#(n__length(L)) → activate^#(L)
length^#(cons(N, L)) → uLength^#(and(isNat(N), isNatList(activate(L))), activate(L))	isNatList^#(n__take(N, IL)) → activate^#(N)
isNatList^#(n__cons(N, L)) → activate^#(N)	isNatIList^#(n__cons(N, IL)) → isNatIList^#(activate(IL))
isNatIList^#(IL) → isNatList^#(activate(IL))	uLength^#(tt, L) → activate^#(L)
isNat^#(n__s(N)) → activate^#(N)	take^#(s(M), cons(N, IL)) → uTake2^#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
isNatIList^#(n__cons(N, IL)) → activate^#(IL)	activate^#(n__length(X)) → length^#(X)
length^#(cons(N, L)) → isNatList^#(activate(L))	uTake2^#(tt, M, N, IL) → activate^#(N)
isNatList^#(n__cons(N, L)) → isNat^#(activate(N))	isNatIList^#(n__cons(N, IL)) → activate^#(N)
activate^#(n__take(X1, X2)) → take^#(X1, X2)	take^#(s(M), cons(N, IL)) → activate^#(IL)
take^#(0, IL) → isNatIList^#(IL)	take^#(s(M), cons(N, IL)) → isNat^#(M)
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