Term Rewriting System R:

   [y, z, x]
   app(f, app(app(cons, nil), y)) -> y
   app(f, app(app(cons, app(f, app(app(cons, nil), y))), z)) -> app(app(app(copy, n), y), z)
   app(app(app(copy, 0), y), z) -> app(f, z)
   app(app(app(copy, app(s, x)), y), z) -> app(app(app(copy, x), y), app(app(cons, app(f, y)), z))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   APP(app(app(copy, app(s, x)), y), z) -> APP(app(app(copy, x), y), app(app(cons, app(f, y)), z))
   APP(app(app(copy, app(s, x)), y), z) -> APP(app(copy, x), y)
   APP(app(app(copy, app(s, x)), y), z) -> APP(copy, x)
   APP(app(app(copy, app(s, x)), y), z) -> APP(app(cons, app(f, y)), z)
   APP(app(app(copy, app(s, x)), y), z) -> APP(cons, app(f, y))
   APP(app(app(copy, app(s, x)), y), z) -> APP(f, y)
   APP(f, app(app(cons, app(f, app(app(cons, nil), y))), z)) -> APP(app(app(copy, n), y), z)
   APP(f, app(app(cons, app(f, app(app(cons, nil), y))), z)) -> APP(app(copy, n), y)
   APP(f, app(app(cons, app(f, app(app(cons, nil), y))), z)) -> APP(copy, n)
   APP(app(app(copy, 0), y), z) -> APP(f, z)

Furthermore, R contains one SCC.


SCC1:

APP(app(app(copy, 0), y), z) -> APP(f, z)
APP(f, app(app(cons, app(f, app(app(cons, nil), y))), z)) -> APP(app(copy, n), y)
APP(f, app(app(cons, app(f, app(app(cons, nil), y))), z)) -> APP(app(app(copy, n), y), z)
APP(app(app(copy, app(s, x)), y), z) -> APP(f, y)
APP(app(app(copy, app(s, x)), y), z) -> APP(app(cons, app(f, y)), z)
APP(app(app(copy, app(s, x)), y), z) -> APP(app(copy, x), y)
APP(app(app(copy, app(s, x)), y), z) -> APP(app(app(copy, x), y), app(app(cons, app(f, y)), z))

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

   APP(app(app(copy, app(s, x)), y), z) -> APP(app(copy, x), y)
no new Dependency Pairs
are created.

none
The transformation is resulting in one subcycle:


SCC1.Nar1:

APP(f, app(app(cons, app(f, app(app(cons, nil), y))), z)) -> APP(app(copy, n), y)
APP(app(app(copy, app(s, x)), y), z) -> APP(f, y)
APP(app(app(copy, app(s, x)), y), z) -> APP(app(cons, app(f, y)), z)
APP(app(app(copy, app(s, x)), y), z) -> APP(app(app(copy, x), y), app(app(cons, app(f, y)), z))
APP(f, app(app(cons, app(f, app(app(cons, nil), y))), z)) -> APP(app(app(copy, n), y), z)
APP(app(app(copy, 0), y), z) -> APP(f, z)

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

   APP(f, app(app(cons, app(f, app(app(cons, nil), y))), z)) -> APP(app(app(copy, n), y), z)
no new Dependency Pairs
are created.

none
The transformation is resulting in one subcycle:


SCC1.Nar1.Nar1:

APP(app(app(copy, 0), y), z) -> APP(f, z)
APP(app(app(copy, app(s, x)), y), z) -> APP(f, y)
APP(app(app(copy, app(s, x)), y), z) -> APP(app(cons, app(f, y)), z)
APP(app(app(copy, app(s, x)), y), z) -> APP(app(app(copy, x), y), app(app(cons, app(f, y)), z))
APP(f, app(app(cons, app(f, app(app(cons, nil), y))), z)) -> APP(app(copy, n), y)

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

   APP(f, app(app(cons, app(f, app(app(cons, nil), y))), z)) -> APP(app(copy, n), y)
no new Dependency Pairs
are created.

none
The transformation is resulting in one subcycle:


SCC1.Nar1.Nar1.Nar1:

APP(app(app(copy, app(s, x)), y), z) -> APP(app(app(copy, x), y), app(app(cons, app(f, y)), z))
APP(app(app(copy, app(s, x)), y), z) -> APP(app(cons, app(f, y)), z)

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

   APP(app(app(copy, app(s, x)), y), z) -> APP(app(cons, app(f, y)), z)
two new Dependency Pairs
are created:


   APP(app(app(copy, app(s, x)), app(app(cons, nil), y'')), z) -> APP(app(cons, y''), z)
   APP(app(app(copy, app(s, x)), app(app(cons, app(f, app(app(cons, nil), y''))), z'')), z) -> APP(app(cons, app(app(app(copy, n), y''), z'')), z)

The transformation is resulting in one subcycle:


SCC1.Nar1.Nar1.Nar1.Nar1:

APP(app(app(copy, app(s, x)), app(app(cons, app(f, app(app(cons, nil), y''))), z'')), z) -> APP(app(cons, app(app(app(copy, n), y''), z'')), z)
APP(app(app(copy, app(s, x)), app(app(cons, nil), y'')), z) -> APP(app(cons, y''), z)
APP(app(app(copy, app(s, x)), y), z) -> APP(app(app(copy, x), y), app(app(cons, app(f, y)), z))

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

   APP(app(app(copy, app(s, x)), app(app(cons, nil), y'')), z) -> APP(app(cons, y''), z)
no new Dependency Pairs
are created.

none
The transformation is resulting in one subcycle:


SCC1.Nar1.Nar1.Nar1.Nar1.Nar1:

APP(app(app(copy, app(s, x)), y), z) -> APP(app(app(copy, x), y), app(app(cons, app(f, y)), z))
APP(app(app(copy, app(s, x)), app(app(cons, app(f, app(app(cons, nil), y''))), z'')), z) -> APP(app(cons, app(app(app(copy, n), y''), z'')), z)

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

   APP(app(app(copy, app(s, x)), app(app(cons, app(f, app(app(cons, nil), y''))), z'')), z) -> APP(app(cons, app(app(app(copy, n), y''), z'')), z)
no new Dependency Pairs
are created.

none
The transformation is resulting in one subcycle:


SCC1.Nar1.Nar1.Nar1.Nar1.Nar1.Nar1:

APP(app(app(copy, app(s, x)), y), z) -> APP(app(app(copy, x), y), app(app(cons, app(f, y)), z))

At least one Dependency Pair of this SCC can be strictly oriented.


The following rules can be oriented: 

   app(f, app(app(cons, nil), y)) -> y
   app(app(app(copy, app(s, x)), y), z) -> app(app(app(copy, x), y), app(app(cons, app(f, y)), z))
   app(f, app(app(cons, app(f, app(app(cons, nil), y))), z)) -> app(app(app(copy, n), y), z)
   app(app(app(copy, 0), y), z) -> app(f, z)


Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
APP > [cons, f, app, n] > copy

 resulting in no new SCCs.

Used Argument Filtering System: ([APP(x_1, x_2) -> APP(x_1, x_2), app(x_1, x_2) -> app(x_1, x_2)])

Termination of R successfully shown.


Duration: 34.608 seconds.