The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (23ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (153ms).
 |    | – Problem 3 was processed with processor DependencyGraph (1ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4 (32ms).

Problem 1: DependencyGraph

---

---

Dependency Pair Problem

Dependency Pairs

f_1#(x, x)	→	f_1#(i_0(x), g_1(g_1(x)))		g_1#(x)	→	T(x)
T(g_1(x_1))	→	T(x_1)		T(g_1(x))	→	g_1#(x)
T(g_1(g_1(x)))	→	g_1#(g_1(x))		f_1#(x, i_0(x))	→	f_1#(x, x)
f_1#(x, y)	→	T(x)		T(i_0(x_1))	→	T(x_1)

Rewrite Rules

f_1(x, x)	→	f_1(i_0(x), g_1(g_1(x)))		f_1(x, i_0(g_1(x)))	→	a_0
f_1(x, y)	→	x		f_1(x, i_0(x))	→	f_1(x, x)
g_1(x)	→	i_0(x)

Original Signature

Termination of terms over the following signature is verified: i_0, a_0, g_1, f_1

Strategy

Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_0) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅
μ(i_0) = {1}

---

The following SCCs where found

g_1#(x) → T(x)	T(g_1(x_1)) → T(x_1)
T(g_1(x)) → g_1#(x)	T(g_1(g_1(x))) → g_1#(g_1(x))
T(i_0(x_1)) → T(x_1)

---

Problem 2: PolynomialLinearRange4

---

---

Dependency Pair Problem

Dependency Pairs

g_1#(x)	→	T(x)		T(g_1(x_1))	→	T(x_1)
T(g_1(x))	→	g_1#(x)		T(g_1(g_1(x)))	→	g_1#(g_1(x))
T(i_0(x_1))	→	T(x_1)

Rewrite Rules

f_1(x, x)	→	f_1(i_0(x), g_1(g_1(x)))		f_1(x, i_0(g_1(x)))	→	a_0
f_1(x, y)	→	x		f_1(x, i_0(x))	→	f_1(x, x)
g_1(x)	→	i_0(x)

Original Signature

Termination of terms over the following signature is verified: i_0, a_0, g_1, f_1

Strategy

Context-sensitive strategy:
μ(T) = μ(a_0) = μ(f_1#) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅
μ(i_0) = {1}

---

Polynomial Interpretation

• T(x): x
• a_0: 0
• f_1(x,y): x + 1
• g_1(x): 2x + 1
• g_1#(x): 2x
• i_0(x): x

Standard Usable rules

g_1(x)	→	i_0(x)		f_1(x, i_0(x))	→	f_1(x, x)
f_1(x, y)	→	x		f_1(x, x)	→	f_1(i_0(x), g_1(g_1(x)))
f_1(x, i_0(g_1(x)))	→	a_0

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

T(g_1(x_1))	→	T(x_1)		T(g_1(g_1(x)))	→	g_1#(g_1(x))
T(g_1(x))	→	g_1#(x)

Problem 3: DependencyGraph

---

---

Dependency Pair Problem

Dependency Pairs

g_1#(x)

→

T(x)

T(i_0(x_1))

→

T(x_1)

Rewrite Rules

f_1(x, x)	→	f_1(i_0(x), g_1(g_1(x)))		f_1(x, i_0(g_1(x)))	→	a_0
f_1(x, y)	→	x		f_1(x, i_0(x))	→	f_1(x, x)
g_1(x)	→	i_0(x)

Original Signature

Termination of terms over the following signature is verified: i_0, a_0, g_1, f_1

Strategy

Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_0) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅
μ(i_0) = {1}

---

The following SCCs where found

T(i_0(x_1)) → T(x_1)

---

Problem 4: PolynomialLinearRange4

---

---

Dependency Pair Problem

Dependency Pairs

T(i_0(x_1))

→

T(x_1)

Rewrite Rules

f_1(x, x)	→	f_1(i_0(x), g_1(g_1(x)))		f_1(x, i_0(g_1(x)))	→	a_0
f_1(x, y)	→	x		f_1(x, i_0(x))	→	f_1(x, x)
g_1(x)	→	i_0(x)

Original Signature

Termination of terms over the following signature is verified: i_0, a_0, g_1, f_1

Strategy

Context-sensitive strategy:
μ(T) = μ(a_0) = μ(f_1#) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅
μ(i_0) = {1}

---

Polynomial Interpretation

• T(x): x
• a_0: 0
• f_1(x,y): 0
• g_1(x): 0
• i_0(x): x + 1

There are no usable rules

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

T(i_0(x_1))

→

T(x_1)