+(1,

+(0,

R

↳Dependency Pair Analysis

+'(1,x) -> +'(+(0, 1),x)

+'(1,x) -> +'(0, 1)

Furthermore,

R

↳DPs

→DP Problem 1

↳Narrowing Transformation

**+'(1, x) -> +'(+(0, 1), x)**

+(1,x) -> +(+(0, 1),x)

+(0,x) ->x

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

As a result of transforming the rule

one new Dependency Pair is created:

+'(1,x) -> +'(+(0, 1),x)

+'(1,x) -> +'(1,x)

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**+'(1, x) -> +'(1, x)**

+(1,x) -> +(+(0, 1),x)

+(0,x) ->x

Duration:

0:00 minutes