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

↳Argument Filtering and Ordering

→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)

The following dependency pairs can be strictly oriented:

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

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

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

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

There are no usable rules w.r.t. to the AFS that need to be oriented.

Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

I > 0

O > 0

+ > 0

+' > 0

resulting in one new DP problem.

Used Argument Filtering System:

+'(x,_{1}x) ->_{2}x_{2}

O(x) -> O(_{1}x)_{1}

I(x) -> I(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****+'(I(***x*), I(*y*)) -> +'(+(*x*,*y*), I(0))**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*)**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*)

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****+'(I(***x*), I(*y*)) -> +'(+(*x*,*y*), I(0))**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*)**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*)

Duration:

0:00 minutes