Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

eq^#(apply(T, S), apply(Tp, Sp))	→	eq^#(T, Tp)	eq^#(lambda(X, T), lambda(Xp, Tp))	→	and^#(eq(T, Tp), eq(X, Xp))
ren^#(var(L), var(K), var(Lp))	→	if^#(eq(L, Lp), var(K), var(Lp))	eq^#(var(L), var(Lp))	→	eq^#(L, Lp)
eq^#(cons(T, L), cons(Tp, Lp))	→	eq^#(T, Tp)	eq^#(apply(T, S), apply(Tp, Sp))	→	and^#(eq(T, Tp), eq(S, Sp))
eq^#(cons(T, L), cons(Tp, Lp))	→	and^#(eq(T, Tp), eq(L, Lp))	eq^#(lambda(X, T), lambda(Xp, Tp))	→	eq^#(T, Tp)
eq^#(cons(T, L), cons(Tp, Lp))	→	eq^#(L, Lp)	eq^#(lambda(X, T), lambda(Xp, Tp))	→	eq^#(X, Xp)
ren^#(X, Y, lambda(Z, T))	→	ren^#(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T)	ren^#(var(L), var(K), var(Lp))	→	eq^#(L, Lp)
ren^#(X, Y, apply(T, S))	→	ren^#(X, Y, T)	ren^#(X, Y, apply(T, S))	→	ren^#(X, Y, S)
eq^#(apply(T, S), apply(Tp, Sp))	→	eq^#(S, Sp)	ren^#(X, Y, lambda(Z, T))	→	ren^#(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T))

Rewrite Rules

and(false, false)	→	false	and(true, false)	→	false
and(false, true)	→	false	and(true, true)	→	true
eq(nil, nil)	→	true	eq(cons(T, L), nil)	→	false
eq(nil, cons(T, L))	→	false	eq(cons(T, L), cons(Tp, Lp))	→	and(eq(T, Tp), eq(L, Lp))
eq(var(L), var(Lp))	→	eq(L, Lp)	eq(var(L), apply(T, S))	→	false
eq(var(L), lambda(X, T))	→	false	eq(apply(T, S), var(L))	→	false
eq(apply(T, S), apply(Tp, Sp))	→	and(eq(T, Tp), eq(S, Sp))	eq(apply(T, S), lambda(X, Tp))	→	false
eq(lambda(X, T), var(L))	→	false	eq(lambda(X, T), apply(Tp, Sp))	→	false
eq(lambda(X, T), lambda(Xp, Tp))	→	and(eq(T, Tp), eq(X, Xp))	if(true, var(K), var(L))	→	var(K)
if(false, var(K), var(L))	→	var(L)	ren(var(L), var(K), var(Lp))	→	if(eq(L, Lp), var(K), var(Lp))
ren(X, Y, apply(T, S))	→	apply(ren(X, Y, T), ren(X, Y, S))	ren(X, Y, lambda(Z, T))	→	lambda(var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), ren(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T)))

Original Signature

Termination of terms over the following signature is verified: apply, lambda, var, if, false, true, ren, and, eq, nil, cons

Strategy

The following SCCs where found

eq^#(lambda(X, T), lambda(Xp, Tp)) → eq^#(T, Tp)	eq^#(apply(T, S), apply(Tp, Sp)) → eq^#(T, Tp)
eq^#(cons(T, L), cons(Tp, Lp)) → eq^#(L, Lp)	eq^#(lambda(X, T), lambda(Xp, Tp)) → eq^#(X, Xp)
eq^#(var(L), var(Lp)) → eq^#(L, Lp)	eq^#(cons(T, L), cons(Tp, Lp)) → eq^#(T, Tp)
eq^#(apply(T, S), apply(Tp, Sp)) → eq^#(S, Sp)

ren^#(X, Y, lambda(Z, T)) → ren^#(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T)	ren^#(X, Y, apply(T, S)) → ren^#(X, Y, T)
ren^#(X, Y, apply(T, S)) → ren^#(X, Y, S)	ren^#(X, Y, lambda(Z, T)) → ren^#(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T))

Problem 2: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

ren^#(X, Y, lambda(Z, T))	→	ren^#(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T)		ren^#(X, Y, apply(T, S))	→	ren^#(X, Y, T)
ren^#(X, Y, apply(T, S))	→	ren^#(X, Y, S)		ren^#(X, Y, lambda(Z, T))	→	ren^#(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T))

Rewrite Rules

and(false, false)	→	false	and(true, false)	→	false
and(false, true)	→	false	and(true, true)	→	true
eq(nil, nil)	→	true	eq(cons(T, L), nil)	→	false
eq(nil, cons(T, L))	→	false	eq(cons(T, L), cons(Tp, Lp))	→	and(eq(T, Tp), eq(L, Lp))
eq(var(L), var(Lp))	→	eq(L, Lp)	eq(var(L), apply(T, S))	→	false
eq(var(L), lambda(X, T))	→	false	eq(apply(T, S), var(L))	→	false
eq(apply(T, S), apply(Tp, Sp))	→	and(eq(T, Tp), eq(S, Sp))	eq(apply(T, S), lambda(X, Tp))	→	false
eq(lambda(X, T), var(L))	→	false	eq(lambda(X, T), apply(Tp, Sp))	→	false
eq(lambda(X, T), lambda(Xp, Tp))	→	and(eq(T, Tp), eq(X, Xp))	if(true, var(K), var(L))	→	var(K)
if(false, var(K), var(L))	→	var(L)	ren(var(L), var(K), var(Lp))	→	if(eq(L, Lp), var(K), var(Lp))
ren(X, Y, apply(T, S))	→	apply(ren(X, Y, T), ren(X, Y, S))	ren(X, Y, lambda(Z, T))	→	lambda(var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), ren(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T)))

Original Signature

Termination of terms over the following signature is verified: apply, lambda, var, if, false, true, ren, and, eq, nil, cons

Strategy

Polynomial Interpretation

and(x,y): x + 1
apply(x,y): 2y + 2x
cons(x,y): 0
eq(x,y): x
false: 1
if(x,y,z): 0
lambda(x,y): y + 2x + 2
nil: 0
ren(x,y,z): z
ren#(x,y,z): z
true: 2
var(x): 0

Improved Usable rules

if(true, var(K), var(L))	→	var(K)	if(false, var(K), var(L))	→	var(L)
ren(X, Y, apply(T, S))	→	apply(ren(X, Y, T), ren(X, Y, S))	ren(X, Y, lambda(Z, T))	→	lambda(var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), ren(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T)))
ren(var(L), var(K), var(Lp))	→	if(eq(L, Lp), var(K), var(Lp))

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

ren^#(X, Y, lambda(Z, T))

→

ren^#(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T)

ren^#(X, Y, lambda(Z, T))

→

ren^#(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T))

Problem 4: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

ren^#(X, Y, apply(T, S))

→

ren^#(X, Y, T)

ren^#(X, Y, apply(T, S))

→

ren^#(X, Y, S)

Rewrite Rules

and(false, false)	→	false	and(true, false)	→	false
and(false, true)	→	false	and(true, true)	→	true
eq(nil, nil)	→	true	eq(cons(T, L), nil)	→	false
eq(nil, cons(T, L))	→	false	eq(cons(T, L), cons(Tp, Lp))	→	and(eq(T, Tp), eq(L, Lp))
eq(var(L), var(Lp))	→	eq(L, Lp)	eq(var(L), apply(T, S))	→	false
eq(var(L), lambda(X, T))	→	false	eq(apply(T, S), var(L))	→	false
eq(apply(T, S), apply(Tp, Sp))	→	and(eq(T, Tp), eq(S, Sp))	eq(apply(T, S), lambda(X, Tp))	→	false
eq(lambda(X, T), var(L))	→	false	eq(lambda(X, T), apply(Tp, Sp))	→	false
eq(lambda(X, T), lambda(Xp, Tp))	→	and(eq(T, Tp), eq(X, Xp))	if(true, var(K), var(L))	→	var(K)
if(false, var(K), var(L))	→	var(L)	ren(var(L), var(K), var(Lp))	→	if(eq(L, Lp), var(K), var(Lp))
ren(X, Y, apply(T, S))	→	apply(ren(X, Y, T), ren(X, Y, S))	ren(X, Y, lambda(Z, T))	→	lambda(var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), ren(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T)))

Original Signature

Termination of terms over the following signature is verified: lambda, apply, if, var, ren, true, false, cons, nil, eq, and

Strategy

Polynomial Interpretation

and(x,y): 0
apply(x,y): 2y + 2x + 1
cons(x,y): 0
eq(x,y): 0
false: 0
if(x,y,z): 0
lambda(x,y): 0
nil: 0
ren(x,y,z): 0
ren#(x,y,z): 2z
true: 0
var(x): 0

There are no usable rules

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

ren^#(X, Y, apply(T, S))

→

ren^#(X, Y, T)

ren^#(X, Y, apply(T, S))

→

ren^#(X, Y, S)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

eq^#(lambda(X, T), lambda(Xp, Tp))	→	eq^#(T, Tp)	eq^#(apply(T, S), apply(Tp, Sp))	→	eq^#(T, Tp)
eq^#(cons(T, L), cons(Tp, Lp))	→	eq^#(L, Lp)	eq^#(lambda(X, T), lambda(Xp, Tp))	→	eq^#(X, Xp)
eq^#(var(L), var(Lp))	→	eq^#(L, Lp)	eq^#(cons(T, L), cons(Tp, Lp))	→	eq^#(T, Tp)
eq^#(apply(T, S), apply(Tp, Sp))	→	eq^#(S, Sp)

Rewrite Rules

and(false, false)	→	false	and(true, false)	→	false
and(false, true)	→	false	and(true, true)	→	true
eq(nil, nil)	→	true	eq(cons(T, L), nil)	→	false
eq(nil, cons(T, L))	→	false	eq(cons(T, L), cons(Tp, Lp))	→	and(eq(T, Tp), eq(L, Lp))
eq(var(L), var(Lp))	→	eq(L, Lp)	eq(var(L), apply(T, S))	→	false
eq(var(L), lambda(X, T))	→	false	eq(apply(T, S), var(L))	→	false
eq(apply(T, S), apply(Tp, Sp))	→	and(eq(T, Tp), eq(S, Sp))	eq(apply(T, S), lambda(X, Tp))	→	false
eq(lambda(X, T), var(L))	→	false	eq(lambda(X, T), apply(Tp, Sp))	→	false
eq(lambda(X, T), lambda(Xp, Tp))	→	and(eq(T, Tp), eq(X, Xp))	if(true, var(K), var(L))	→	var(K)
if(false, var(K), var(L))	→	var(L)	ren(var(L), var(K), var(Lp))	→	if(eq(L, Lp), var(K), var(Lp))
ren(X, Y, apply(T, S))	→	apply(ren(X, Y, T), ren(X, Y, S))	ren(X, Y, lambda(Z, T))	→	lambda(var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), ren(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil)))), T)))

Original Signature

Termination of terms over the following signature is verified: apply, lambda, var, if, false, true, ren, and, eq, nil, cons

Strategy

Projection

The following projection was used:

π (eq#): 1

Thus, the following dependency pairs are removed:

eq^#(apply(T, S), apply(Tp, Sp))	→	eq^#(T, Tp)	eq^#(lambda(X, T), lambda(Xp, Tp))	→	eq^#(T, Tp)
eq^#(lambda(X, T), lambda(Xp, Tp))	→	eq^#(X, Xp)	eq^#(cons(T, L), cons(Tp, Lp))	→	eq^#(L, Lp)
eq^#(var(L), var(Lp))	→	eq^#(L, Lp)	eq^#(cons(T, L), cons(Tp, Lp))	→	eq^#(T, Tp)
eq^#(apply(T, S), apply(Tp, Sp))	→	eq^#(S, Sp)

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: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

Polynomial Interpretation

Improved Usable rules

Problem 4: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

Polynomial Interpretation

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

Rewrite Rules

Original Signature

Strategy

Projection