f(f(

R

↳Dependency Pair Analysis

F(f(y,z), f(x, f(a,x))) -> F(f(f(a,z), f(x, a)), f(a,y))

F(f(y,z), f(x, f(a,x))) -> F(f(a,z), f(x, a))

F(f(y,z), f(x, f(a,x))) -> F(a,z)

F(f(y,z), f(x, f(a,x))) -> F(x, a)

F(f(y,z), f(x, f(a,x))) -> F(a,y)

Furthermore,

R

↳DPs

→DP Problem 1

↳Usable Rules (Innermost)

**F(f( y, z), f(x, f(a, x))) -> F(f(f(a, z), f(x, a)), f(a, y))**

f(f(y,z), f(x, f(a,x))) -> f(f(f(a,z), f(x, a)), f(a,y))

innermost

As we are in the innermost case, we can delete all 1 non-usable-rules.

R

↳DPs

→DP Problem 1

↳UsableRules

→DP Problem 2

↳Semantic Labelling

**F(f( y, z), f(x, f(a, x))) -> F(f(f(a, z), f(x, a)), f(a, y))**

none

innermost

Using Semantic Labelling, the DP problem could be transformed. The following model was found:

F(x_{0}, x_{1})= 1 f(x_{0}, x_{1})= 1 + x _{1}a= 0

From the dependency graph we obtain 0 (labeled) SCCs which each result in correspondingDP problem.

Duration:

0:00 minutes