MAYBE

The TRS could not be proven terminating. The proof attempt took 4633 ms.

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (0ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (11ms), PolynomialLinearRange4iUR (691ms), DependencyGraph (9ms), PolynomialLinearRange8NegiUR (2633ms), DependencyGraph (10ms), ReductionPairSAT (920ms), DependencyGraph (9ms), SizeChangePrinciple (107ms)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

a^#(p(x, y), z)	→	a^#(y, z)		a^#(p(x, y), z)	→	a^#(x, z)
a^#(a(x, y), z)	→	a^#(y, z)		a^#(lambda(x), y)	→	a^#(x, p(1, a(y, t)))
a^#(a(x, y), z)	→	a^#(x, a(y, z))		a^#(lambda(x), y)	→	a^#(y, t)

Rewrite Rules

a(lambda(x), y)	→	lambda(a(x, p(1, a(y, t))))		a(p(x, y), z)	→	p(a(x, z), a(y, z))
a(a(x, y), z)	→	a(x, a(y, z))		lambda(x)	→	x
a(x, y)	→	x		a(x, y)	→	y
p(x, y)	→	x		p(x, y)	→	y

Original Signature

Termination of terms over the following signature is verified: lambda, 1, t, a, p

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

a^#(p(x, y), z)	→	a^#(x, z)		a^#(p(x, y), z)	→	a^#(y, z)
a^#(a(x, y), z)	→	a^#(y, z)		a^#(lambda(x), y)	→	a^#(x, p(1, a(y, t)))
a^#(p(x, y), z)	→	p^#(a(x, z), a(y, z))		a^#(lambda(x), y)	→	p^#(1, a(y, t))
a^#(lambda(x), y)	→	lambda^#(a(x, p(1, a(y, t))))		a^#(a(x, y), z)	→	a^#(x, a(y, z))
a^#(lambda(x), y)	→	a^#(y, t)

Rewrite Rules

a(lambda(x), y)	→	lambda(a(x, p(1, a(y, t))))		a(p(x, y), z)	→	p(a(x, z), a(y, z))
a(a(x, y), z)	→	a(x, a(y, z))		lambda(x)	→	x
a(x, y)	→	x		a(x, y)	→	y
p(x, y)	→	x		p(x, y)	→	y

Original Signature

Termination of terms over the following signature is verified: lambda, 1, t, p, a

Strategy

The following SCCs where found

a^#(p(x, y), z) → a^#(x, z)	a^#(p(x, y), z) → a^#(y, z)
a^#(a(x, y), z) → a^#(y, z)	a^#(lambda(x), y) → a^#(x, p(1, a(y, t)))
a^#(a(x, y), z) → a^#(x, a(y, z))	a^#(lambda(x), y) → a^#(y, t)