Term Rewriting System R:
[x, y, z]
rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

REV(++(x, y)) -> ++'(rev(y), rev(x))
REV(++(x, y)) -> REV(y)
REV(++(x, y)) -> REV(x)
++'(.(x, y), z) -> ++'(y, z)
++'(x, ++(y, z)) -> ++'(++(x, y), z)
++'(x, ++(y, z)) -> ++'(x, y)

Furthermore, R contains two SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Narrowing Transformation
       →DP Problem 2
         ↳Remaining


Dependency Pairs:

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


Rules:


rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

++'(x, ++(y, z)) -> ++'(++(x, y), z)
three new Dependency Pairs are created:

++'(nil, ++(y'', z)) -> ++'(y'', z)
++'(.(x'', y''), ++(y0, z)) -> ++'(.(x'', ++(y'', y0)), z)
++'(x'', ++(++(y'', z''), z)) -> ++'(++(++(x'', y''), z''), z)

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 3
             ↳Forward Instantiation Transformation
       →DP Problem 2
         ↳Remaining


Dependency Pairs:

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


Rules:


rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

++'(.(x, y), z) -> ++'(y, z)
four new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 3
             ↳FwdInst
             ...
               →DP Problem 4
                 ↳Forward Instantiation Transformation
       →DP Problem 2
         ↳Remaining


Dependency Pairs:

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


Rules:


rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)


Strategy:

innermost




On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

++'(x, ++(y, z)) -> ++'(x, y)
seven new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
       →DP Problem 2
         ↳Remaining Obligation(s)




The following remains to be proven:


   R
     ↳DPs
       →DP Problem 1
         ↳Nar
       →DP Problem 2
         ↳Remaining Obligation(s)




The following remains to be proven:

Innermost Termination of R could not be shown.
Duration:
0:10 minutes