:(

:(

:(:(

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

↳Narrowing Transformation

**:'(:( 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

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,y0), :(x'',y'')) -> :'(x, :(x'', :(i(y0), i(y''))))

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

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

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

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 5

↳Narrowing Transformation

**:'(:( x, y0), :(x'', i(x'''))) -> :'(x, :(x'', :(i(y0), 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

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

As a result of transforming the rule

three new Dependency Pairs are created:

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

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

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 6

↳Narrowing Transformation

**:'(:( x, :(x'', y'')), e) -> :'(x, i(:(y'', 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

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

As a result of transforming the rule

six new Dependency Pairs are created:

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

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

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

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

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

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 7

↳Narrowing Transformation

**:'(:( x, :(x''', y''')), e) -> :'(x, i(:(y''', 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

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

As a result of transforming the rule

three new Dependency Pairs are created:

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

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

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 8

↳Narrowing Transformation

**:'(:( x, i(x''')), :(x'0, y')) -> :'(x, :(x'0, :(x''', 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

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 9

↳Forward Instantiation Transformation

**:'(:( x, :(x''', y''')), e) -> :'(x, i(:(y''', 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

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

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 10

↳Forward Instantiation Transformation

**:'(:( x, i(x''')), :(x'0, y')) -> :'(x, :(x'0, :(x''', 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 Forward Instantiation SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 11

↳Forward Instantiation Transformation

**:'(e, :( x'', y'')) -> I(:(x'', 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 Forward Instantiation SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 12

↳Forward Instantiation Transformation

**:'(:( x, i(x''')), :(x'0, y')) -> :'(x, :(x'0, :(x''', 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 Forward Instantiation SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 13

↳Forward Instantiation Transformation

**:'(e, :( x'', y'')) -> I(:(x'', 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 Forward Instantiation SCC transformation can be performed.

As a result of transforming the rule

three new Dependency Pairs are created:

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

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

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 14

↳Argument Filtering and Ordering

**:'(:( x, i(x''')), :(x'0, y')) -> :'(x, :(x'0, :(x''', 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

The following dependency pairs can be strictly oriented:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

The following usable rules for innermost w.r.t. to the AFS can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(:(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(I(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(i(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(e)= 0 _{ }^{ }_{ }^{ }POL(:'(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }

resulting in one new DP problem.

Used Argument Filtering System:

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

:(x,_{1}x) -> :(_{2}x,_{1}x)_{2}

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

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

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 15

↳Dependency Graph

**:'(:( x, i(x''')), :(x'0, y')) -> :'(x, :(x'0, :(x''', 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

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:08 minutes