Term Rewriting System R:
[f, xs, x, y, ys]
ap(ap(map, f), xs) -> ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) -> null
ap(ap(ap(if, null), f), xs) -> ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) -> ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) -> true
ap(isEmpty, ap(ap(cons, x), xs)) -> null
ap(last, ap(ap(cons, x), null)) -> x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) -> null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

AP(ap(map, f), xs) -> AP(ap(ap(if, ap(isEmpty, xs)), f), xs)
AP(ap(map, f), xs) -> AP(ap(if, ap(isEmpty, xs)), f)
AP(ap(map, f), xs) -> AP(if, ap(isEmpty, xs))
AP(ap(map, f), xs) -> AP(isEmpty, xs)
AP(ap(ap(if, null), f), xs) -> AP(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
AP(ap(ap(if, null), f), xs) -> AP(cons, ap(f, ap(last, xs)))
AP(ap(ap(if, null), f), xs) -> AP(f, ap(last, xs))
AP(ap(ap(if, null), f), xs) -> AP(last, xs)
AP(ap(ap(if, null), f), xs) -> AP(ap(if2, f), xs)
AP(ap(ap(if, null), f), xs) -> AP(if2, f)
AP(ap(if2, f), xs) -> AP(ap(map, f), ap(dropLast, xs))
AP(ap(if2, f), xs) -> AP(map, f)
AP(ap(if2, f), xs) -> AP(dropLast, xs)
AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(last, ap(ap(cons, y), ys))
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(dropLast, ap(ap(cons, y), ys))

Furthermore, R contains three SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Usable Rules (Innermost)
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules


Dependency Pair:

AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(last, ap(ap(cons, y), ys))


Rules:


ap(ap(map, f), xs) -> ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) -> null
ap(ap(ap(if, null), f), xs) -> ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) -> ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) -> true
ap(isEmpty, ap(ap(cons, x), xs)) -> null
ap(last, ap(ap(cons, x), null)) -> x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) -> null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))


Strategy:

innermost




As we are in the innermost case, we can delete all 10 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 4
             ↳A-Transformation
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules


Dependency Pair:

AP(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(last, ap(ap(cons, y), ys))


Rule:

none


Strategy:

innermost




We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 4
             ↳ATrans
             ...
               →DP Problem 5
                 ↳Size-Change Principle
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules


Dependency Pair:

LAST(cons(x, cons(y, ys))) -> LAST(cons(y, ys))


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. LAST(cons(x, cons(y, ys))) -> LAST(cons(y, ys))
and get the following Size-Change Graph(s):
{1} , {1}
1>1

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳Usable Rules (Innermost)
       →DP Problem 3
         ↳UsableRules


Dependency Pair:

AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(dropLast, ap(ap(cons, y), ys))


Rules:


ap(ap(map, f), xs) -> ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) -> null
ap(ap(ap(if, null), f), xs) -> ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) -> ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) -> true
ap(isEmpty, ap(ap(cons, x), xs)) -> null
ap(last, ap(ap(cons, x), null)) -> x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) -> null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))


Strategy:

innermost




As we are in the innermost case, we can delete all 10 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 6
             ↳A-Transformation
       →DP Problem 3
         ↳UsableRules


Dependency Pair:

AP(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> AP(dropLast, ap(ap(cons, y), ys))


Rule:

none


Strategy:

innermost




We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 6
             ↳ATrans
             ...
               →DP Problem 7
                 ↳Size-Change Principle
       →DP Problem 3
         ↳UsableRules


Dependency Pair:

DROPLAST(cons(x, cons(y, ys))) -> DROPLAST(cons(y, ys))


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. DROPLAST(cons(x, cons(y, ys))) -> DROPLAST(cons(y, ys))
and get the following Size-Change Graph(s):
{1} , {1}
1>1

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳Usable Rules (Innermost)


Dependency Pairs:

AP(ap(if2, f), xs) -> AP(ap(map, f), ap(dropLast, xs))
AP(ap(ap(if, null), f), xs) -> AP(ap(if2, f), xs)
AP(ap(ap(if, null), f), xs) -> AP(f, ap(last, xs))
AP(ap(map, f), xs) -> AP(ap(ap(if, ap(isEmpty, xs)), f), xs)


Rules:


ap(ap(map, f), xs) -> ap(ap(ap(if, ap(isEmpty, xs)), f), xs)
ap(ap(ap(if, true), f), xs) -> null
ap(ap(ap(if, null), f), xs) -> ap(ap(cons, ap(f, ap(last, xs))), ap(ap(if2, f), xs))
ap(ap(if2, f), xs) -> ap(ap(map, f), ap(dropLast, xs))
ap(isEmpty, null) -> true
ap(isEmpty, ap(ap(cons, x), xs)) -> null
ap(last, ap(ap(cons, x), null)) -> x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) -> null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))


Strategy:

innermost




As we are in the innermost case, we can delete all 4 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 8
             ↳Narrowing Transformation


Dependency Pairs:

AP(ap(if2, f), xs) -> AP(ap(map, f), ap(dropLast, xs))
AP(ap(ap(if, null), f), xs) -> AP(ap(if2, f), xs)
AP(ap(ap(if, null), f), xs) -> AP(f, ap(last, xs))
AP(ap(map, f), xs) -> AP(ap(ap(if, ap(isEmpty, xs)), f), xs)


Rules:


ap(dropLast, ap(ap(cons, x), null)) -> null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
ap(last, ap(ap(cons, x), null)) -> x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(last, ap(ap(cons, y), ys))
ap(isEmpty, null) -> true
ap(isEmpty, ap(ap(cons, x), xs)) -> null


Strategy:

innermost




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

AP(ap(map, f), xs) -> AP(ap(ap(if, ap(isEmpty, xs)), f), xs)
two new Dependency Pairs are created:

AP(ap(map, f), null) -> AP(ap(ap(if, true), f), null)
AP(ap(map, f), ap(ap(cons, x'), xs'')) -> AP(ap(ap(if, null), f), ap(ap(cons, x'), xs''))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

AP(ap(ap(if, null), f), xs) -> AP(ap(if2, f), xs)
AP(ap(ap(if, null), f), xs) -> AP(f, ap(last, xs))
AP(ap(map, f), ap(ap(cons, x'), xs'')) -> AP(ap(ap(if, null), f), ap(ap(cons, x'), xs''))
AP(ap(if2, f), xs) -> AP(ap(map, f), ap(dropLast, xs))


Rules:


ap(dropLast, ap(ap(cons, x), null)) -> null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
ap(last, ap(ap(cons, x), null)) -> x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(last, ap(ap(cons, y), ys))
ap(isEmpty, null) -> true
ap(isEmpty, ap(ap(cons, x), xs)) -> null


Strategy:

innermost




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

AP(ap(if2, f), xs) -> AP(ap(map, f), ap(dropLast, xs))
two new Dependency Pairs are created:

AP(ap(if2, f), ap(ap(cons, x'), null)) -> AP(ap(map, f), null)
AP(ap(if2, f), ap(ap(cons, x'), ap(ap(cons, y'), ys'))) -> AP(ap(map, f), ap(ap(cons, x'), ap(dropLast, ap(ap(cons, y'), ys'))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 8
             ↳Nar
             ...
               →DP Problem 10
                 ↳Usable Rules (Innermost)


Dependency Pairs:

AP(ap(ap(if, null), f), xs) -> AP(f, ap(last, xs))
AP(ap(map, f), ap(ap(cons, x'), xs'')) -> AP(ap(ap(if, null), f), ap(ap(cons, x'), xs''))
AP(ap(if2, f), ap(ap(cons, x'), ap(ap(cons, y'), ys'))) -> AP(ap(map, f), ap(ap(cons, x'), ap(dropLast, ap(ap(cons, y'), ys'))))
AP(ap(ap(if, null), f), xs) -> AP(ap(if2, f), xs)


Rules:


ap(dropLast, ap(ap(cons, x), null)) -> null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
ap(last, ap(ap(cons, x), null)) -> x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(last, ap(ap(cons, y), ys))
ap(isEmpty, null) -> true
ap(isEmpty, ap(ap(cons, x), xs)) -> null


Strategy:

innermost




As we are in the innermost case, we can delete all 2 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 8
             ↳Nar
             ...
               →DP Problem 11
                 ↳Modular Removal of Rules


Dependency Pairs:

AP(ap(ap(if, null), f), xs) -> AP(f, ap(last, xs))
AP(ap(map, f), ap(ap(cons, x'), xs'')) -> AP(ap(ap(if, null), f), ap(ap(cons, x'), xs''))
AP(ap(if2, f), ap(ap(cons, x'), ap(ap(cons, y'), ys'))) -> AP(ap(map, f), ap(ap(cons, x'), ap(dropLast, ap(ap(cons, y'), ys'))))
AP(ap(ap(if, null), f), xs) -> AP(ap(if2, f), xs)


Rules:


ap(last, ap(ap(cons, x), null)) -> x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) -> null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))


Strategy:

innermost




We have the following set of usable rules:

ap(last, ap(ap(cons, x), null)) -> x
ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) -> null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(last)=  0  
  POL(if)=  0  
  POL(dropLast)=  0  
  POL(ap(x1, x2))=  x1 + x2  
  POL(null)=  1  
  POL(cons)=  0  
  POL(map)=  1  
  POL(if2)=  1  
  POL(AP(x1, x2))=  1 + x1 + x2  

We have the following set D of usable symbols: {last, if, dropLast, null, cons, ap, map, if2, AP}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

AP(ap(ap(if, null), f), xs) -> AP(f, ap(last, xs))

The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

ap(last, ap(ap(cons, x), null)) -> x


The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 8
             ↳Nar
             ...
               →DP Problem 12
                 ↳Modular Removal of Rules


Dependency Pairs:

AP(ap(map, f), ap(ap(cons, x'), xs'')) -> AP(ap(ap(if, null), f), ap(ap(cons, x'), xs''))
AP(ap(if2, f), ap(ap(cons, x'), ap(ap(cons, y'), ys'))) -> AP(ap(map, f), ap(ap(cons, x'), ap(dropLast, ap(ap(cons, y'), ys'))))
AP(ap(ap(if, null), f), xs) -> AP(ap(if2, f), xs)


Rules:


ap(last, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(last, ap(ap(cons, y), ys))
ap(dropLast, ap(ap(cons, x), null)) -> null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))


Strategy:

innermost




The original DP problem is in applicative form. Its DPs and usable rules are the following.

AP(ap(map, f), ap(ap(cons, x'), xs'')) -> AP(ap(ap(if, null), f), ap(ap(cons, x'), xs''))
AP(ap(if2, f), ap(ap(cons, x'), ap(ap(cons, y'), ys'))) -> AP(ap(map, f), ap(ap(cons, x'), ap(dropLast, ap(ap(cons, y'), ys'))))
AP(ap(ap(if, null), f), xs) -> AP(ap(if2, f), xs)


ap(dropLast, ap(ap(cons, x), null)) -> null
ap(dropLast, ap(ap(cons, x), ap(ap(cons, y), ys))) -> ap(ap(cons, x), ap(dropLast, ap(ap(cons, y), ys)))


It is proper and hence, it can be A-transformed which results in the DP problem

MAP(f, cons(x', xs'')) -> IF(null, f, cons(x', xs''))
IF2(f, cons(x', cons(y', ys'))) -> MAP(f, cons(x', dropLast(cons(y', ys'))))
IF(null, f, xs) -> IF2(f, xs)


dropLast(cons(x, null)) -> null
dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))


To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(MAP(x1, x2))=  x1 + x2  
  POL(dropLast(x1))=  x1  
  POL(cons(x1, x2))=  x1 + x2  
  POL(null)=  0  
  POL(IF(x1, x2, x3))=  x1 + x2 + x3  
  POL(IF2(x1, x2))=  x1 + x2  

We have the following set D of usable symbols: {MAP, dropLast, cons, null, IF, IF2}
No Dependency Pairs can be deleted.
1 non usable rules have been deleted.

The result of this processor delivers one new DP problem.
Note that we keep the A-transformed DP problem as result of this processor.



   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 8
             ↳Nar
             ...
               →DP Problem 13
                 ↳Modular Removal of Rules


Dependency Pairs:

MAP(f, cons(x', xs'')) -> IF(null, f, cons(x', xs''))
IF2(f, cons(x', cons(y', ys'))) -> MAP(f, cons(x', dropLast(cons(y', ys'))))
IF(null, f, xs) -> IF2(f, xs)


Rules:


dropLast(cons(x, null)) -> null
dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))


Strategy:

innermost




We have the following set of usable rules:

dropLast(cons(x, null)) -> null
dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(MAP(x1, x2))=  x1 + x2  
  POL(dropLast(x1))=  x1  
  POL(cons(x1, x2))=  1 + x1 + x2  
  POL(null)=  0  
  POL(IF(x1, x2, x3))=  x1 + x2 + x3  
  POL(IF2(x1, x2))=  x1 + x2  

We have the following set D of usable symbols: {MAP, dropLast, cons, null, IF, IF2}
No Dependency Pairs can be deleted.
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

dropLast(cons(x, null)) -> null


The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 8
             ↳Nar
             ...
               →DP Problem 14
                 ↳Instantiation Transformation


Dependency Pairs:

MAP(f, cons(x', xs'')) -> IF(null, f, cons(x', xs''))
IF2(f, cons(x', cons(y', ys'))) -> MAP(f, cons(x', dropLast(cons(y', ys'))))
IF(null, f, xs) -> IF2(f, xs)


Rule:


dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))


Strategy:

innermost




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

IF(null, f, xs) -> IF2(f, xs)
one new Dependency Pair is created:

IF(null, f'', cons(x''', xs'''')) -> IF2(f'', cons(x''', xs''''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 8
             ↳Nar
             ...
               →DP Problem 15
                 ↳Negative Polynomial Order


Dependency Pairs:

IF2(f, cons(x', cons(y', ys'))) -> MAP(f, cons(x', dropLast(cons(y', ys'))))
IF(null, f'', cons(x''', xs'''')) -> IF2(f'', cons(x''', xs''''))
MAP(f, cons(x', xs'')) -> IF(null, f, cons(x', xs''))


Rule:


dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))


Strategy:

innermost




The following Dependency Pair can be strictly oriented using the given order.

IF2(f, cons(x', cons(y', ys'))) -> MAP(f, cons(x', dropLast(cons(y', ys'))))


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))


Used ordering:
Polynomial Order with Interpretation:

POL( IF2(x1, x2) ) = max{0, x2 - 1}

POL( cons(x1, x2) ) = x2 + 1

POL( MAP(x1, x2) ) = max{0, x2 - 1}

POL( dropLast(x1) ) = max{0, x1 - 1}

POL( IF(x1, ..., x3) ) = max{0, x3 - 1}


This results in one new DP problem. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 8
             ↳Nar
             ...
               →DP Problem 16
                 ↳Dependency Graph


Dependency Pairs:

IF(null, f'', cons(x''', xs'''')) -> IF2(f'', cons(x''', xs''''))
MAP(f, cons(x', xs'')) -> IF(null, f, cons(x', xs''))


Rule:


dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys)))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:08 minutes