f(

f(

f(

f(i(

g(

R

↳Dependency Pair Analysis

F(x,x) -> F(i(x), g(g(x)))

F(x,x) -> G(g(x))

F(x,x) -> G(x)

F(x, i(x)) -> F(x,x)

Furthermore,

R

↳DPs

→DP Problem 1

↳Rewriting Transformation

**F( x, i(x)) -> F(x, x)**

f(x,x) -> f(i(x), g(g(x)))

f(x,y) ->x

f(x, i(x)) -> f(x,x)

f(i(x), i(g(x))) -> a

g(x) -> i(x)

innermost

On this DP problem, a Rewriting SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

F(x,x) -> F(i(x), g(g(x)))

F(x,x) -> F(i(x), i(g(x)))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Rw

→DP Problem 2

↳Rewriting Transformation

**F( x, x) -> F(i(x), i(g(x)))**

f(x,x) -> f(i(x), g(g(x)))

f(x,y) ->x

f(x, i(x)) -> f(x,x)

f(i(x), i(g(x))) -> a

g(x) -> i(x)

innermost

On this DP problem, a Rewriting SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

F(x,x) -> F(i(x), i(g(x)))

F(x,x) -> F(i(x), i(i(x)))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Rw

→DP Problem 2

↳Rw

...

→DP Problem 3

↳Instantiation Transformation

**F( x, x) -> F(i(x), i(i(x)))**

f(x,x) -> f(i(x), g(g(x)))

f(x,y) ->x

f(x, i(x)) -> f(x,x)

f(i(x), i(g(x))) -> a

g(x) -> i(x)

innermost

On this DP problem, an Instantiation SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

F(x, i(x)) -> F(x,x)

F(i(x''), i(i(x''))) -> F(i(x''), i(x''))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Rw

→DP Problem 2

↳Rw

...

→DP Problem 4

↳Instantiation Transformation

**F(i( x''), i(i(x''))) -> F(i(x''), i(x''))**

f(x,x) -> f(i(x), g(g(x)))

f(x,y) ->x

f(x, i(x)) -> f(x,x)

f(i(x), i(g(x))) -> a

g(x) -> i(x)

innermost

On this DP problem, an Instantiation SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

F(x,x) -> F(i(x), i(i(x)))

F(i(x''''), i(x'''')) -> F(i(i(x'''')), i(i(i(x''''))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Rw

→DP Problem 2

↳Rw

...

→DP Problem 5

↳Remaining Obligation(s)

The following remains to be proven:

**F(i( x''''), i(x'''')) -> F(i(i(x'''')), i(i(i(x''''))))**

f(x,x) -> f(i(x), g(g(x)))

f(x,y) ->x

f(x, i(x)) -> f(x,x)

f(i(x), i(g(x))) -> a

g(x) -> i(x)

innermost

Duration:

0:00 minutes