.(1,

.(

.(i(

.(

.(i(

.(

.(.(

i(1) -> 1

i(i(

i(.(

R

↳Dependency Pair Analysis

.'(.(x,y),z) -> .'(x, .(y,z))

.'(.(x,y),z) -> .'(y,z)

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

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

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pairs:****.'(.(***x*,*y*),*z*) -> .'(*y*,*z*)**.'(.(***x*,*y*),*z*) -> .'(*x*, .(*y*,*z*))**Rules:**

.(1,*x*) ->*x*

.(*x*, 1) ->*x*

.(i(*x*),*x*) -> 1

.(*x*, i(*x*)) -> 1

.(i(*y*), .(*y*,*z*)) ->*z*

.(*y*, .(i(*y*),*z*)) ->*z*

.(.(*x*,*y*),*z*) -> .(*x*, .(*y*,*z*))

i(1) -> 1

i(i(*x*)) ->*x*

i(.(*x*,*y*)) -> .(i(*y*), i(*x*))**Dependency Pairs:****I(.(***x*,*y*)) -> I(*x*)**I(.(***x*,*y*)) -> I(*y*)**Rules:**

.(1,*x*) ->*x*

.(*x*, 1) ->*x*

.(i(*x*),*x*) -> 1

.(*x*, i(*x*)) -> 1

.(i(*y*), .(*y*,*z*)) ->*z*

.(*y*, .(i(*y*),*z*)) ->*z*

.(.(*x*,*y*),*z*) -> .(*x*, .(*y*,*z*))

i(1) -> 1

i(i(*x*)) ->*x*

i(.(*x*,*y*)) -> .(i(*y*), i(*x*))

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pairs:****.'(.(***x*,*y*),*z*) -> .'(*y*,*z*)**.'(.(***x*,*y*),*z*) -> .'(*x*, .(*y*,*z*))**Rules:**

.(1,*x*) ->*x*

.(*x*, 1) ->*x*

.(i(*x*),*x*) -> 1

.(*x*, i(*x*)) -> 1

.(i(*y*), .(*y*,*z*)) ->*z*

.(*y*, .(i(*y*),*z*)) ->*z*

.(.(*x*,*y*),*z*) -> .(*x*, .(*y*,*z*))

i(1) -> 1

i(i(*x*)) ->*x*

i(.(*x*,*y*)) -> .(i(*y*), i(*x*))**Dependency Pairs:****I(.(***x*,*y*)) -> I(*x*)**I(.(***x*,*y*)) -> I(*y*)**Rules:**

.(1,*x*) ->*x*

.(*x*, 1) ->*x*

.(i(*x*),*x*) -> 1

.(*x*, i(*x*)) -> 1

.(i(*y*), .(*y*,*z*)) ->*z*

.(*y*, .(i(*y*),*z*)) ->*z*

.(.(*x*,*y*),*z*) -> .(*x*, .(*y*,*z*))

i(1) -> 1

i(i(*x*)) ->*x*

i(.(*x*,*y*)) -> .(i(*y*), i(*x*))

Duration:

0:00 minutes