:(

:(

:(:(

:(e,

:(

:(

:(i(

:(i(

i(:(

i(i(

i(e) -> e

R

↳Dependency Pair Analysis

:'(:(x,y),z) -> :'(x, :(z, i(y)))

:'(:(x,y),z) -> :'(z, i(y))

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

:'(e,x) -> I(x)

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

:'(x, :(y, :(i(x),z))) -> :'(i(z),y)

:'(x, :(y, :(i(x),z))) -> I(z)

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

:'(i(x), :(y, :(x,z))) -> :'(i(z),y)

:'(i(x), :(y, :(x,z))) -> I(z)

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Narrowing Transformation

**:'(i( x), :(y, :(x, z))) -> I(z)**

:(x,x) -> e

:(x, e) ->x

:(:(x,y),z) -> :(x, :(z, i(y)))

:(e,x) -> i(x)

:(x, :(y, i(x))) -> i(y)

:(x, :(y, :(i(x),z))) -> :(i(z),y)

:(i(x), :(y,x)) -> i(y)

:(i(x), :(y, :(x,z))) -> :(i(z),y)

i(:(x,y)) -> :(y,x)

i(i(x)) ->x

i(e) -> e

innermost

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

As a result of transforming the rule

five new Dependency Pairs are created:

:'(:(x,y),z) -> :'(x, :(z, i(y)))

:'(:(x,y'), i(y')) -> :'(x, e)

:'(:(x,y0), :(x'',y'')) -> :'(x, :(x'', :(i(y0), i(y''))))

:'(:(x,y'), e) -> :'(x, i(i(y')))

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

:'(:(x, i(x'')),z) -> :'(x, :(z,x''))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Narrowing Transformation

**:'(:( x, y'), e) -> :'(x, i(i(y')))**

:(x,x) -> e

:(x, e) ->x

:(:(x,y),z) -> :(x, :(z, i(y)))

:(e,x) -> i(x)

:(x, :(y, i(x))) -> i(y)

:(x, :(y, :(i(x),z))) -> :(i(z),y)

:(i(x), :(y,x)) -> i(y)

:(i(x), :(y, :(x,z))) -> :(i(z),y)

i(:(x,y)) -> :(y,x)

i(i(x)) ->x

i(e) -> e

innermost

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

As a result of transforming the rule

two new Dependency Pairs are created:

:'(x, :(y, :(i(x),z))) -> :'(i(z),y)

:'(x, :(y, :(i(x), :(x'',y'')))) -> :'(:(y'',x''),y)

:'(x, :(y, :(i(x), i(x'')))) -> :'(x'',y)

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 3

↳Narrowing Transformation

**:'(:( x, y0), :(x'', y'')) -> :'(x, :(x'', :(i(y0), i(y''))))**

:(x,x) -> e

:(x, e) ->x

:(:(x,y),z) -> :(x, :(z, i(y)))

:(e,x) -> i(x)

:(x, :(y, i(x))) -> i(y)

:(x, :(y, :(i(x),z))) -> :(i(z),y)

:(i(x), :(y,x)) -> i(y)

:(i(x), :(y, :(x,z))) -> :(i(z),y)

i(:(x,y)) -> :(y,x)

i(i(x)) ->x

i(e) -> e

innermost

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

As a result of transforming the rule

two new Dependency Pairs are created:

:'(i(x), :(y, :(x,z))) -> :'(i(z),y)

:'(i(x), :(y, :(x, :(x'',y'')))) -> :'(:(y'',x''),y)

:'(i(x), :(y, :(x, i(x'')))) -> :'(x'',y)

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 4

↳Remaining Obligation(s)

The following remains to be proven:

**:'(:( x, i(x'')), z) -> :'(x, :(z, x''))**

:(x,x) -> e

:(x, e) ->x

:(:(x,y),z) -> :(x, :(z, i(y)))

:(e,x) -> i(x)

:(x, :(y, i(x))) -> i(y)

:(x, :(y, :(i(x),z))) -> :(i(z),y)

:(i(x), :(y,x)) -> i(y)

:(i(x), :(y, :(x,z))) -> :(i(z),y)

i(:(x,y)) -> :(y,x)

i(i(x)) ->x

i(e) -> e

innermost

Duration:

0:01 minutes