O(0) -> 0

+(0,

+(

+(O(

+(O(

+(I(

+(I(

*(0,

*(

*(O(

*(I(

R

↳Dependency Pair Analysis

+'(O(x), O(y)) -> O'(+(x,y))

+'(O(x), O(y)) -> +'(x,y)

+'(O(x), I(y)) -> +'(x,y)

+'(I(x), O(y)) -> +'(x,y)

+'(I(x), I(y)) -> O'(+(+(x,y), I(0)))

+'(I(x), I(y)) -> +'(+(x,y), I(0))

+'(I(x), I(y)) -> +'(x,y)

*'(O(x),y) -> O'(*(x,y))

*'(O(x),y) -> *'(x,y)

*'(I(x),y) -> +'(O(*(x,y)),y)

*'(I(x),y) -> O'(*(x,y))

*'(I(x),y) -> *'(x,y)

Furthermore,

R

↳DPs

→DP Problem 1

↳Narrowing Transformation

→DP Problem 2

↳Remaining

**+'(I( x), I(y)) -> +'(x, y)**

O(0) -> 0

+(0,x) ->x

+(x, 0) ->x

+(O(x), O(y)) -> O(+(x,y))

+(O(x), I(y)) -> I(+(x,y))

+(I(x), O(y)) -> I(+(x,y))

+(I(x), I(y)) -> O(+(+(x,y), I(0)))

*(0,x) -> 0

*(x, 0) -> 0

*(O(x),y) -> O(*(x,y))

*(I(x),y) -> +(O(*(x,y)),y)

innermost

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

As a result of transforming the rule

six new Dependency Pairs are created:

+'(I(x), I(y)) -> +'(+(x,y), I(0))

+'(I(0), I(y')) -> +'(y', I(0))

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

+'(I(O(x'')), I(O(y''))) -> +'(O(+(x'',y'')), I(0))

+'(I(O(x'')), I(I(y''))) -> +'(I(+(x'',y'')), I(0))

+'(I(I(x'')), I(O(y''))) -> +'(I(+(x'',y'')), I(0))

+'(I(I(x'')), I(I(y''))) -> +'(O(+(+(x'',y''), I(0))), I(0))

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:

**Dependency Pairs:****+'(I(I(***x''*)), I(I(*y''*))) -> +'(O(+(+(*x''*,*y''*), I(0))), I(0))**+'(I(I(***x''*)), I(O(*y''*))) -> +'(I(+(*x''*,*y''*)), I(0))**+'(I(O(***x''*)), I(I(*y''*))) -> +'(I(+(*x''*,*y''*)), I(0))**+'(I(O(***x''*)), I(O(*y''*))) -> +'(O(+(*x''*,*y''*)), I(0))**+'(I(***x''*), I(0)) -> +'(*x''*, I(0))**+'(I(0), I(***y'*)) -> +'(*y'*, I(0))**+'(I(***x*), O(*y*)) -> +'(*x*,*y*)**+'(O(***x*), I(*y*)) -> +'(*x*,*y*)**+'(O(***x*), O(*y*)) -> +'(*x*,*y*)**+'(I(***x*), I(*y*)) -> +'(*x*,*y*)**Rules:**

O(0) -> 0

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

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

+(O(*x*), O(*y*)) -> O(+(*x*,*y*))

+(O(*x*), I(*y*)) -> I(+(*x*,*y*))

+(I(*x*), O(*y*)) -> I(+(*x*,*y*))

+(I(*x*), I(*y*)) -> O(+(+(*x*,*y*), I(0)))

*(0,*x*) -> 0

*(*x*, 0) -> 0

*(O(*x*),*y*) -> O(*(*x*,*y*))

*(I(*x*),*y*) -> +(O(*(*x*,*y*)),*y*)**Strategy:**innermost

**Dependency Pairs:*****'(I(***x*),*y*) -> *'(*x*,*y*)***'(O(***x*),*y*) -> *'(*x*,*y*)**Rules:**

O(0) -> 0

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

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

+(O(*x*), O(*y*)) -> O(+(*x*,*y*))

+(O(*x*), I(*y*)) -> I(+(*x*,*y*))

+(I(*x*), O(*y*)) -> I(+(*x*,*y*))

+(I(*x*), I(*y*)) -> O(+(+(*x*,*y*), I(0)))

*(0,*x*) -> 0

*(*x*, 0) -> 0

*(O(*x*),*y*) -> O(*(*x*,*y*))

*(I(*x*),*y*) -> +(O(*(*x*,*y*)),*y*)**Strategy:**innermost

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pairs:****+'(I(I(***x''*)), I(I(*y''*))) -> +'(O(+(+(*x''*,*y''*), I(0))), I(0))**+'(I(I(***x''*)), I(O(*y''*))) -> +'(I(+(*x''*,*y''*)), I(0))**+'(I(O(***x''*)), I(I(*y''*))) -> +'(I(+(*x''*,*y''*)), I(0))**+'(I(O(***x''*)), I(O(*y''*))) -> +'(O(+(*x''*,*y''*)), I(0))**+'(I(***x''*), I(0)) -> +'(*x''*, I(0))**+'(I(0), I(***y'*)) -> +'(*y'*, I(0))**+'(I(***x*), O(*y*)) -> +'(*x*,*y*)**+'(O(***x*), I(*y*)) -> +'(*x*,*y*)**+'(O(***x*), O(*y*)) -> +'(*x*,*y*)**+'(I(***x*), I(*y*)) -> +'(*x*,*y*)**Rules:**

O(0) -> 0

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

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

+(O(*x*), O(*y*)) -> O(+(*x*,*y*))

+(O(*x*), I(*y*)) -> I(+(*x*,*y*))

+(I(*x*), O(*y*)) -> I(+(*x*,*y*))

+(I(*x*), I(*y*)) -> O(+(+(*x*,*y*), I(0)))

*(0,*x*) -> 0

*(*x*, 0) -> 0

*(O(*x*),*y*) -> O(*(*x*,*y*))

*(I(*x*),*y*) -> +(O(*(*x*,*y*)),*y*)**Strategy:**innermost

**Dependency Pairs:*****'(I(***x*),*y*) -> *'(*x*,*y*)***'(O(***x*),*y*) -> *'(*x*,*y*)**Rules:**

O(0) -> 0

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

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

+(O(*x*), O(*y*)) -> O(+(*x*,*y*))

+(O(*x*), I(*y*)) -> I(+(*x*,*y*))

+(I(*x*), O(*y*)) -> I(+(*x*,*y*))

+(I(*x*), I(*y*)) -> O(+(+(*x*,*y*), I(0)))

*(0,*x*) -> 0

*(*x*, 0) -> 0

*(O(*x*),*y*) -> O(*(*x*,*y*))

*(I(*x*),*y*) -> +(O(*(*x*,*y*)),*y*)**Strategy:**innermost

Duration:

0:00 minutes