O(0) -> 0

+(0,

+(

+(O(

+(O(

+(I(

+(I(

*(0,

*(

*(O(

*(I(

-(

-(0,

-(O(

-(O(

-(I(

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

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

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

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

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

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

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

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

→DP Problem 3

↳Remaining Obligation(s)

The following remains to be proven:

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

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

-(0,*x*) -> 0

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

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

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

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

**Dependency Pairs:****-'(I(***x*), I(*y*)) -> -'(*x*,*y*)**-'(I(***x*), O(*y*)) -> -'(*x*,*y*)**-'(O(***x*), I(*y*)) -> -'(*x*,*y*)**-'(O(***x*), I(*y*)) -> -'(-(*x*,*y*), I(1))**-'(O(***x*), O(*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*)

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

-(0,*x*) -> 0

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

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

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

-(I(*x*), I(*y*)) -> O(-(*x*,*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*)

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

-(0,*x*) -> 0

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

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

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

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

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

→DP Problem 3

↳Remaining Obligation(s)

The following remains to be proven:

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

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

-(0,*x*) -> 0

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

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

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

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

**Dependency Pairs:****-'(I(***x*), I(*y*)) -> -'(*x*,*y*)**-'(I(***x*), O(*y*)) -> -'(*x*,*y*)**-'(O(***x*), I(*y*)) -> -'(*x*,*y*)**-'(O(***x*), I(*y*)) -> -'(-(*x*,*y*), I(1))**-'(O(***x*), O(*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*)

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

-(0,*x*) -> 0

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

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

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

-(I(*x*), I(*y*)) -> O(-(*x*,*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*)

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

-(0,*x*) -> 0

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

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

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

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

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

→DP Problem 3

↳Remaining Obligation(s)

The following remains to be proven:

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

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

-(0,*x*) -> 0

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

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

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

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

**Dependency Pairs:****-'(I(***x*), I(*y*)) -> -'(*x*,*y*)**-'(I(***x*), O(*y*)) -> -'(*x*,*y*)**-'(O(***x*), I(*y*)) -> -'(*x*,*y*)**-'(O(***x*), I(*y*)) -> -'(-(*x*,*y*), I(1))**-'(O(***x*), O(*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*)

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

-(0,*x*) -> 0

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

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

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

-(I(*x*), I(*y*)) -> O(-(*x*,*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*)

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

-(0,*x*) -> 0

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

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

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

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

Duration:

0:00 minutes