Term Rewriting System R:
[x, l, y]
app(rev, nil) -> nil
app(rev, app(app(cons, x), l)) -> app(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
app(app(rev1, 0), nil) -> 0
app(app(rev1, app(s, x)), nil) -> app(s, x)
app(app(rev1, x), app(app(cons, y), l)) -> app(app(rev1, y), l)
app(app(rev2, x), nil) -> nil
app(app(rev2, x), app(app(cons, y), l)) -> app(rev, app(app(cons, x), app(app(rev2, y), l)))

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

APP(rev, app(app(cons, x), l)) -> APP(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
APP(rev, app(app(cons, x), l)) -> APP(cons, app(app(rev1, x), l))
APP(rev, app(app(cons, x), l)) -> APP(app(rev1, x), l)
APP(rev, app(app(cons, x), l)) -> APP(rev1, x)
APP(rev, app(app(cons, x), l)) -> APP(app(rev2, x), l)
APP(rev, app(app(cons, x), l)) -> APP(rev2, x)
APP(app(rev1, x), app(app(cons, y), l)) -> APP(app(rev1, y), l)
APP(app(rev1, x), app(app(cons, y), l)) -> APP(rev1, y)
APP(app(rev2, x), app(app(cons, y), l)) -> APP(rev, app(app(cons, x), app(app(rev2, y), l)))
APP(app(rev2, x), app(app(cons, y), l)) -> APP(app(cons, x), app(app(rev2, y), l))
APP(app(rev2, x), app(app(cons, y), l)) -> APP(cons, x)
APP(app(rev2, x), app(app(cons, y), l)) -> APP(app(rev2, y), l)
APP(app(rev2, x), app(app(cons, y), l)) -> APP(rev2, y)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Narrowing Transformation


Dependency Pairs:

APP(app(rev2, x), app(app(cons, y), l)) -> APP(app(rev2, y), l)
APP(app(rev2, x), app(app(cons, y), l)) -> APP(app(cons, x), app(app(rev2, y), l))
APP(app(rev2, x), app(app(cons, y), l)) -> APP(rev, app(app(cons, x), app(app(rev2, y), l)))
APP(app(rev1, x), app(app(cons, y), l)) -> APP(app(rev1, y), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev2, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev1, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))


Rules:


app(rev, nil) -> nil
app(rev, app(app(cons, x), l)) -> app(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
app(app(rev1, 0), nil) -> 0
app(app(rev1, app(s, x)), nil) -> app(s, x)
app(app(rev1, x), app(app(cons, y), l)) -> app(app(rev1, y), l)
app(app(rev2, x), nil) -> nil
app(app(rev2, x), app(app(cons, y), l)) -> app(rev, app(app(cons, x), app(app(rev2, y), l)))





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

APP(app(rev2, x), app(app(cons, y), l)) -> APP(app(cons, x), app(app(rev2, y), l))
two new Dependency Pairs are created:

APP(app(rev2, x), app(app(cons, y'), nil)) -> APP(app(cons, x), nil)
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''), l''))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(rev2, y''), l''))))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''), l''))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(rev2, y''), l''))))
APP(app(rev2, x), app(app(cons, y), l)) -> APP(rev, app(app(cons, x), app(app(rev2, y), l)))
APP(app(rev1, x), app(app(cons, y), l)) -> APP(app(rev1, y), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev2, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev1, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
APP(app(rev2, x), app(app(cons, y), l)) -> APP(app(rev2, y), l)


Rules:


app(rev, nil) -> nil
app(rev, app(app(cons, x), l)) -> app(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
app(app(rev1, 0), nil) -> 0
app(app(rev1, app(s, x)), nil) -> app(s, x)
app(app(rev1, x), app(app(cons, y), l)) -> app(app(rev1, y), l)
app(app(rev2, x), nil) -> nil
app(app(rev2, x), app(app(cons, y), l)) -> app(rev, app(app(cons, x), app(app(rev2, y), l)))





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

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''), l''))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(rev2, y''), l''))))
three new Dependency Pairs are created:

APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), l'''))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(app(rev2, y'''), l'''))), app(app(rev2, y0'), app(app(rev2, y'''), l'''))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), nil))) -> APP(app(cons, x), app(rev, app(app(cons, y0), nil)))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y'), l')))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(app(rev2, y'), l'))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 3
                 ↳Narrowing Transformation


Dependency Pairs:

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y'), l')))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(app(rev2, y'), l'))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), nil))) -> APP(app(cons, x), app(rev, app(app(cons, y0), nil)))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), l'''))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(app(rev2, y'''), l'''))), app(app(rev2, y0'), app(app(rev2, y'''), l'''))))
APP(app(rev2, x), app(app(cons, y), l)) -> APP(app(rev2, y), l)
APP(app(rev1, x), app(app(cons, y), l)) -> APP(app(rev1, y), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev2, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev1, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
APP(app(rev2, x), app(app(cons, y), l)) -> APP(rev, app(app(cons, x), app(app(rev2, y), l)))


Rules:


app(rev, nil) -> nil
app(rev, app(app(cons, x), l)) -> app(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
app(app(rev1, 0), nil) -> 0
app(app(rev1, app(s, x)), nil) -> app(s, x)
app(app(rev1, x), app(app(cons, y), l)) -> app(app(rev1, y), l)
app(app(rev2, x), nil) -> nil
app(app(rev2, x), app(app(cons, y), l)) -> app(rev, app(app(cons, x), app(app(rev2, y), l)))





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

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), nil))) -> APP(app(cons, x), app(rev, app(app(cons, y0), nil)))
one new Dependency Pair is created:

APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), nil))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), nil)), app(app(rev2, y0'), nil)))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 4
                 ↳Narrowing Transformation


Dependency Pairs:

APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), nil))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), nil)), app(app(rev2, y0'), nil)))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), l'''))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(app(rev2, y'''), l'''))), app(app(rev2, y0'), app(app(rev2, y'''), l'''))))
APP(app(rev2, x), app(app(cons, y), l)) -> APP(app(rev2, y), l)
APP(app(rev2, x), app(app(cons, y), l)) -> APP(rev, app(app(cons, x), app(app(rev2, y), l)))
APP(app(rev1, x), app(app(cons, y), l)) -> APP(app(rev1, y), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev2, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev1, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y'), l')))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(app(rev2, y'), l'))))))


Rules:


app(rev, nil) -> nil
app(rev, app(app(cons, x), l)) -> app(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
app(app(rev1, 0), nil) -> 0
app(app(rev1, app(s, x)), nil) -> app(s, x)
app(app(rev1, x), app(app(cons, y), l)) -> app(app(rev1, y), l)
app(app(rev2, x), nil) -> nil
app(app(rev2, x), app(app(cons, y), l)) -> app(rev, app(app(cons, x), app(app(rev2, y), l)))





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

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y'), l')))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(app(rev2, y'), l'))))))
four new Dependency Pairs are created:

APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''), l'')))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(app(rev2, y''), l''))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(app(rev2, y''), l''))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''), l'')))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(app(rev2, y''), l''))), app(app(rev2, y''''), app(app(rev2, y''), l''))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), nil)))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), nil)))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1), l''))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(app(rev2, y1), l''))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 5
                 ↳Narrowing Transformation


Dependency Pairs:

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1), l''))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(app(rev2, y1), l''))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), nil)))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), nil)))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''), l'')))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(app(rev2, y''), l''))), app(app(rev2, y''''), app(app(rev2, y''), l''))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''), l'')))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(app(rev2, y''), l''))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(app(rev2, y''), l''))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), l'''))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(app(rev2, y'''), l'''))), app(app(rev2, y0'), app(app(rev2, y'''), l'''))))
APP(app(rev2, x), app(app(cons, y), l)) -> APP(app(rev2, y), l)
APP(app(rev2, x), app(app(cons, y), l)) -> APP(rev, app(app(cons, x), app(app(rev2, y), l)))
APP(app(rev1, x), app(app(cons, y), l)) -> APP(app(rev1, y), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev2, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev1, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), nil))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), nil)), app(app(rev2, y0'), nil)))


Rules:


app(rev, nil) -> nil
app(rev, app(app(cons, x), l)) -> app(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
app(app(rev1, 0), nil) -> 0
app(app(rev1, app(s, x)), nil) -> app(s, x)
app(app(rev1, x), app(app(cons, y), l)) -> app(app(rev1, y), l)
app(app(rev2, x), nil) -> nil
app(app(rev2, x), app(app(cons, y), l)) -> app(rev, app(app(cons, x), app(app(rev2, y), l)))





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

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), nil)))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), nil)))))
two new Dependency Pairs are created:

APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''), nil)))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), nil)))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), nil)))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''), nil)))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), nil)), app(app(rev2, y''''), nil)))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 6
                 ↳Narrowing Transformation


Dependency Pairs:

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''), nil)))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), nil)), app(app(rev2, y''''), nil)))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''), nil)))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), nil)))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), nil)))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''), l'')))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(app(rev2, y''), l''))), app(app(rev2, y''''), app(app(rev2, y''), l''))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''), l'')))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(app(rev2, y''), l''))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(app(rev2, y''), l''))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), nil))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), nil)), app(app(rev2, y0'), nil)))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), l'''))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(app(rev2, y'''), l'''))), app(app(rev2, y0'), app(app(rev2, y'''), l'''))))
APP(app(rev2, x), app(app(cons, y), l)) -> APP(app(rev2, y), l)
APP(app(rev2, x), app(app(cons, y), l)) -> APP(rev, app(app(cons, x), app(app(rev2, y), l)))
APP(app(rev1, x), app(app(cons, y), l)) -> APP(app(rev1, y), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev2, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev1, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1), l''))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(app(rev2, y1), l''))))))))


Rules:


app(rev, nil) -> nil
app(rev, app(app(cons, x), l)) -> app(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
app(app(rev1, 0), nil) -> 0
app(app(rev1, app(s, x)), nil) -> app(s, x)
app(app(rev1, x), app(app(cons, y), l)) -> app(app(rev1, y), l)
app(app(rev2, x), nil) -> nil
app(app(rev2, x), app(app(cons, y), l)) -> app(rev, app(app(cons, x), app(app(rev2, y), l)))





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

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1), l''))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(app(rev2, y1), l''))))))))
five new Dependency Pairs are created:

APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), l'''))))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), l'''))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))), app(app(rev2, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''''), app(app(cons, y1'), l'''))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(app(cons, app(app(rev1, y''''), app(app(rev2, y1'), l'''))), app(app(rev2, y''''), app(app(rev2, y1'), l'''))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1'), nil))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), nil)))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1'), app(app(cons, y'), l')))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(rev, app(app(cons, y1'), app(app(rev2, y'), l'))))))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 7
                 ↳Narrowing Transformation


Dependency Pairs:

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1'), app(app(cons, y'), l')))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(rev, app(app(cons, y1'), app(app(rev2, y'), l'))))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1'), nil))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), nil)))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''''), app(app(cons, y1'), l'''))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(app(cons, app(app(rev1, y''''), app(app(rev2, y1'), l'''))), app(app(rev2, y''''), app(app(rev2, y1'), l'''))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), l'''))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))), app(app(rev2, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), l'''))))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''), nil)))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), nil)))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), nil)))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''), l'')))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(app(rev2, y''), l''))), app(app(rev2, y''''), app(app(rev2, y''), l''))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''), l'')))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(app(rev2, y''), l''))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(app(rev2, y''), l''))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), nil))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), nil)), app(app(rev2, y0'), nil)))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), l'''))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(app(rev2, y'''), l'''))), app(app(rev2, y0'), app(app(rev2, y'''), l'''))))
APP(app(rev2, x), app(app(cons, y), l)) -> APP(app(rev2, y), l)
APP(app(rev2, x), app(app(cons, y), l)) -> APP(rev, app(app(cons, x), app(app(rev2, y), l)))
APP(app(rev1, x), app(app(cons, y), l)) -> APP(app(rev1, y), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev2, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev1, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''), nil)))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), nil)), app(app(rev2, y''''), nil)))))


Rules:


app(rev, nil) -> nil
app(rev, app(app(cons, x), l)) -> app(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
app(app(rev1, 0), nil) -> 0
app(app(rev1, app(s, x)), nil) -> app(s, x)
app(app(rev1, x), app(app(cons, y), l)) -> app(app(rev1, y), l)
app(app(rev2, x), nil) -> nil
app(app(rev2, x), app(app(cons, y), l)) -> app(rev, app(app(cons, x), app(app(rev2, y), l)))





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

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1'), nil))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), nil)))))))
three new Dependency Pairs are created:

APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), nil))))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), nil)))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), nil)))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), nil))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(rev, app(app(cons, y''0), nil)))), app(app(rev2, y''''), app(rev, app(app(cons, y''0), nil)))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''''), app(app(cons, y1'), nil))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(app(cons, app(app(rev1, y''''), nil)), app(app(rev2, y''''), nil)))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 8
                 ↳Narrowing Transformation


Dependency Pairs:

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''''), app(app(cons, y1'), nil))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(app(cons, app(app(rev1, y''''), nil)), app(app(rev2, y''''), nil)))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), nil))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(rev, app(app(cons, y''0), nil)))), app(app(rev2, y''''), app(rev, app(app(cons, y''0), nil)))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), nil))))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), nil)))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), nil)))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''''), app(app(cons, y1'), l'''))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(app(cons, app(app(rev1, y''''), app(app(rev2, y1'), l'''))), app(app(rev2, y''''), app(app(rev2, y1'), l'''))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), l'''))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))), app(app(rev2, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), l'''))))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''), nil)))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), nil)), app(app(rev2, y''''), nil)))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''), nil)))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), nil)))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), nil)))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''), l'')))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(app(rev2, y''), l''))), app(app(rev2, y''''), app(app(rev2, y''), l''))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''), l'')))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(app(rev2, y''), l''))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(app(rev2, y''), l''))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), nil))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), nil)), app(app(rev2, y0'), nil)))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), l'''))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(app(rev2, y'''), l'''))), app(app(rev2, y0'), app(app(rev2, y'''), l'''))))
APP(app(rev2, x), app(app(cons, y), l)) -> APP(app(rev2, y), l)
APP(app(rev2, x), app(app(cons, y), l)) -> APP(rev, app(app(cons, x), app(app(rev2, y), l)))
APP(app(rev1, x), app(app(cons, y), l)) -> APP(app(rev1, y), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev2, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev1, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1'), app(app(cons, y'), l')))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(rev, app(app(cons, y1'), app(app(rev2, y'), l'))))))))))


Rules:


app(rev, nil) -> nil
app(rev, app(app(cons, x), l)) -> app(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
app(app(rev1, 0), nil) -> 0
app(app(rev1, app(s, x)), nil) -> app(s, x)
app(app(rev1, x), app(app(cons, y), l)) -> app(app(rev1, y), l)
app(app(rev2, x), nil) -> nil
app(app(rev2, x), app(app(cons, y), l)) -> app(rev, app(app(cons, x), app(app(rev2, y), l)))





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

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1'), app(app(cons, y'), l')))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(rev, app(app(cons, y1'), app(app(rev2, y'), l'))))))))))
six new Dependency Pairs are created:

APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1''), app(app(cons, y'0), l'')))))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), app(rev, app(app(cons, y1''), app(app(rev2, y'0), l''))))))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), app(rev, app(app(cons, y1''), app(app(rev2, y'0), l''))))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1''), app(app(cons, y'0), l'')))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(rev, app(app(cons, y''0), app(rev, app(app(cons, y1''), app(app(rev2, y'0), l''))))))), app(app(rev2, y''''), app(rev, app(app(cons, y''0), app(rev, app(app(cons, y1''), app(app(rev2, y'0), l''))))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''''), app(app(cons, y1''), app(app(cons, y'0), l'')))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(app(cons, app(app(rev1, y''''), app(rev, app(app(cons, y1''), app(app(rev2, y'0), l''))))), app(app(rev2, y''''), app(rev, app(app(cons, y1''), app(app(rev2, y'0), l''))))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1''), app(app(cons, y'0), l'')))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(app(cons, app(app(rev1, y1''), app(app(rev2, y'0), l''))), app(app(rev2, y1''), app(app(rev2, y'0), l''))))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1'), app(app(cons, y'0), nil)))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(rev, app(app(cons, y1'), nil)))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1'), app(app(cons, y'0), app(app(cons, y1), l''))))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(rev, app(app(cons, y1'), app(rev, app(app(cons, y'0), app(app(rev2, y1), l''))))))))))))

The transformation is resulting in one new DP problem: 



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




The following remains to be proven:
Dependency Pairs:

APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1'), app(app(cons, y'0), app(app(cons, y1), l''))))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(rev, app(app(cons, y1'), app(rev, app(app(cons, y'0), app(app(rev2, y1), l''))))))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1'), app(app(cons, y'0), nil)))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(rev, app(app(cons, y1'), nil)))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''), app(app(cons, y1''), app(app(cons, y'0), l'')))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(rev, app(app(cons, y''), app(app(cons, app(app(rev1, y1''), app(app(rev2, y'0), l''))), app(app(rev2, y1''), app(app(rev2, y'0), l''))))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''''), app(app(cons, y1''), app(app(cons, y'0), l'')))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(app(cons, app(app(rev1, y''''), app(rev, app(app(cons, y1''), app(app(rev2, y'0), l''))))), app(app(rev2, y''''), app(rev, app(app(cons, y1''), app(app(rev2, y'0), l''))))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1''), app(app(cons, y'0), l'')))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(rev, app(app(cons, y''0), app(rev, app(app(cons, y1''), app(app(rev2, y'0), l''))))))), app(app(rev2, y''''), app(rev, app(app(cons, y''0), app(rev, app(app(cons, y1''), app(app(rev2, y'0), l''))))))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1''), app(app(cons, y'0), l'')))))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), app(rev, app(app(cons, y1''), app(app(rev2, y'0), l''))))))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), app(rev, app(app(cons, y1''), app(app(rev2, y'0), l''))))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), nil))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(rev, app(app(cons, y''0), nil)))), app(app(rev2, y''''), app(rev, app(app(cons, y''0), nil)))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), nil))))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), nil)))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), nil)))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''''), app(app(cons, y1'), l'''))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(app(cons, app(app(rev1, y''''), app(app(rev2, y1'), l'''))), app(app(rev2, y''''), app(app(rev2, y1'), l'''))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), l'''))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))), app(app(rev2, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''0), app(app(cons, y1'), l'''))))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(rev, app(app(cons, y''0), app(app(rev2, y1'), l'''))))))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''), nil)))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), nil)), app(app(rev2, y''''), nil)))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''), nil)))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), nil)))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), nil)))))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y''''), app(app(cons, y''), l'')))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(app(cons, app(app(rev1, y''''), app(app(rev2, y''), l''))), app(app(rev2, y''''), app(app(rev2, y''), l''))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y''''), app(app(cons, y''), l'')))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(rev, app(app(cons, y''''), app(app(rev2, y''), l''))))), app(app(rev2, y0'), app(rev, app(app(cons, y''''), app(app(rev2, y''), l''))))))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), nil))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), nil)), app(app(rev2, y0'), nil)))
APP(app(rev2, x), app(app(cons, y0'), app(app(cons, y'''), l'''))) -> APP(app(cons, x), app(app(cons, app(app(rev1, y0'), app(app(rev2, y'''), l'''))), app(app(rev2, y0'), app(app(rev2, y'''), l'''))))
APP(app(rev2, x), app(app(cons, y), l)) -> APP(app(rev2, y), l)
APP(app(rev2, x), app(app(cons, y), l)) -> APP(rev, app(app(cons, x), app(app(rev2, y), l)))
APP(app(rev1, x), app(app(cons, y), l)) -> APP(app(rev1, y), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev2, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(rev1, x), l)
APP(rev, app(app(cons, x), l)) -> APP(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
APP(app(rev2, x), app(app(cons, y0), app(app(cons, y'''), app(app(cons, y''''), app(app(cons, y1'), nil))))) -> APP(app(cons, x), app(rev, app(app(cons, y0), app(rev, app(app(cons, y'''), app(app(cons, app(app(rev1, y''''), nil)), app(app(rev2, y''''), nil)))))))


Rules:


app(rev, nil) -> nil
app(rev, app(app(cons, x), l)) -> app(app(cons, app(app(rev1, x), l)), app(app(rev2, x), l))
app(app(rev1, 0), nil) -> 0
app(app(rev1, app(s, x)), nil) -> app(s, x)
app(app(rev1, x), app(app(cons, y), l)) -> app(app(rev1, y), l)
app(app(rev2, x), nil) -> nil
app(app(rev2, x), app(app(cons, y), l)) -> app(rev, app(app(cons, x), app(app(rev2, y), l)))




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