Termination Proof using AProVE

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)))

Termination of R to be shown.

     ↳Overlay and local confluence Check

The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.

     ↳OC

       →TRS2

         ↳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.

     ↳OC

       →TRS2

         ↳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.

     ↳OC

       →TRS2

         ↳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.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

...

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

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

D_P: empty set
Oriented Rules: none

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

trivial

with Argument Filtering System:

cons(x₁, x₂) -> cons(x₁, x₂)

We obtain no new DP problems.

     ↳OC

       →TRS2

         ↳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.

     ↳OC

       →TRS2

         ↳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.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

...

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

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

D_P: empty set
Oriented Rules: none

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

trivial

with Argument Filtering System:

cons(x₁, x₂) -> cons(x₁, x₂)

We obtain no new DP problems.

     ↳OC

       →TRS2

         ↳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.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

...

               →DP Problem 8

                 ↳Narrowing Transformation

Dependency Pairs:

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:

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

...

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

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

...

               →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.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

...

               →DP Problem 11

                 ↳Modular Removal of Rules

Dependency Pairs:

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 C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

POL(last) = 0

POL(if) = 0

POL(dropLast) = 0

POL(ap(x₁, x₂)) = x₁ + x₂

POL(null) = 1

POL(cons) = 0

POL(map) = 1

POL(if2) = 1

POL(AP(x₁, x₂)) = 1 + x₁ + x₂

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.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

...

               →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(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 C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

POL(MAP(x₁, x₂)) = x₁ + x₂

POL(dropLast(x₁)) = x₁

POL(cons(x₁, x₂)) = x₁ + x₂

POL(null) = 0

POL(IF(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(IF2(x₁, x₂)) = x₁ + x₂

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.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

...

               →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 C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

POL(MAP(x₁, x₂)) = x₁ + x₂

POL(dropLast(x₁)) = x₁

POL(cons(x₁, x₂)) = 1 + x₁ + x₂

POL(null) = 0

POL(IF(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(IF2(x₁, x₂)) = x₁ + x₂

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.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

...

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

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

...

               →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(x₁, x₂) ) = max{0, x₂ - 1}

POL( cons(x₁, x₂) ) = x₂ + 1

POL( MAP(x₁, x₂) ) = max{0, x₂ - 1}

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

POL( IF(x₁, ..., x₃) ) = max{0, x₃ - 1}

This results in one new DP problem.

     ↳OC

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳UsableRules

           →DP Problem 2

             ↳UsableRules

           →DP Problem 3

             ↳UsableRules

...

               →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.

Termination of R successfully shown.
Duration:
0:10 minutes

POL(last)	= 0
POL(if)	= 0
POL(dropLast)	= 0
POL(ap(x₁, x₂))	= x₁ + x₂
POL(null)	= 1
POL(cons)	= 0
POL(map)	= 1
POL(if2)	= 1
POL(AP(x₁, x₂))	= 1 + x₁ + x₂

POL(MAP(x₁, x₂))	= x₁ + x₂
POL(dropLast(x₁))	= x₁
POL(cons(x₁, x₂))	= x₁ + x₂
POL(null)	= 0
POL(IF(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(IF2(x₁, x₂))	= x₁ + x₂