The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (0ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (0ms).
 |    | – Problem 3 was processed with processor DependencyGraph (0ms).
 |    |    | – Problem 4 remains open; application of the following processors failed [PolynomialLinearRange4iUR (834ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (7124ms), DependencyGraph (1ms), ReductionPairSAT (5351ms), DependencyGraph (2ms), SizeChangePrinciple (53ms)].

The following open problems remain:

Open Dependency Pair Problem 4

Dependency Pairs

c^#(b(y, c(x)))

→

c^#(c(b(a(0, 0), y)))

c^#(b(y, c(x)))

→

c^#(b(a(0, 0), y))

Rewrite Rules

a(x, y)	→	b(x, b(0, c(y)))		c(b(y, c(x)))	→	c(c(b(a(0, 0), y)))
b(y, 0)	→	y

Original Signature

Termination of terms over the following signature is verified: 0, b, c, a

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

a^#(x, y)	→	b^#(x, b(0, c(y)))	c^#(b(y, c(x)))	→	c^#(c(b(a(0, 0), y)))
c^#(b(y, c(x)))	→	c^#(b(a(0, 0), y))	a^#(x, y)	→	c^#(y)
a^#(x, y)	→	b^#(0, c(y))	c^#(b(y, c(x)))	→	a^#(0, 0)
c^#(b(y, c(x)))	→	b^#(a(0, 0), y)

Rewrite Rules

a(x, y)	→	b(x, b(0, c(y)))		c(b(y, c(x)))	→	c(c(b(a(0, 0), y)))
b(y, 0)	→	y

Original Signature

Termination of terms over the following signature is verified: 0, b, c, a

Strategy

The following SCCs where found

c^#(b(y, c(x))) → c^#(c(b(a(0, 0), y)))	c^#(b(y, c(x))) → c^#(b(a(0, 0), y))
a^#(x, y) → c^#(y)	c^#(b(y, c(x))) → a^#(0, 0)

Problem 2: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

c^#(b(y, c(x)))	→	c^#(c(b(a(0, 0), y)))		c^#(b(y, c(x)))	→	c^#(b(a(0, 0), y))
a^#(x, y)	→	c^#(y)		c^#(b(y, c(x)))	→	a^#(0, 0)

Rewrite Rules

a(x, y)	→	b(x, b(0, c(y)))		c(b(y, c(x)))	→	c(c(b(a(0, 0), y)))
b(y, 0)	→	y

Original Signature

Termination of terms over the following signature is verified: 0, b, c, a

Strategy

Polynomial Interpretation

0: 0
a(x,y): x + 2
a#(x,y): y + 2x
b(x,y): y + x
c(x): 2
c#(x): x

Improved Usable rules

a(x, y)	→	b(x, b(0, c(y)))		b(y, 0)	→	y
c(b(y, c(x)))	→	c(c(b(a(0, 0), y)))

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

c^#(b(y, c(x)))

→

a^#(0, 0)

Problem 3: DependencyGraph

Dependency Pair Problem

Dependency Pairs

c^#(b(y, c(x)))	→	c^#(b(a(0, 0), y))		c^#(b(y, c(x)))	→	c^#(c(b(a(0, 0), y)))
a^#(x, y)	→	c^#(y)

Rewrite Rules

a(x, y)	→	b(x, b(0, c(y)))		c(b(y, c(x)))	→	c(c(b(a(0, 0), y)))
b(y, 0)	→	y

Original Signature

Termination of terms over the following signature is verified: 0, b, c, a

Strategy

The following SCCs where found

c^#(b(y, c(x))) → c^#(b(a(0, 0), y))

c^#(b(y, c(x))) → c^#(c(b(a(0, 0), y)))