Termination Proof using AProVE

Term Rewriting System R:
[x, l, l1, l2]
is_empty(nil) -> true
is_empty(cons(x, l)) -> false
hd(cons(x, l)) -> x
tl(cons(x, l)) -> l
append(l1, l2) -> ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) -> l2
ifappend(l1, l2, false) -> cons(hd(l1), append(tl(l1), l2))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

APPEND(l1, l2) -> IFAPPEND(l1, l2, is_empty(l1))
APPEND(l1, l2) -> IS_EMPTY(l1)
IFAPPEND(l1, l2, false) -> HD(l1)
IFAPPEND(l1, l2, false) -> APPEND(tl(l1), l2)
IFAPPEND(l1, l2, false) -> TL(l1)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Usable Rules (Innermost)

Dependency Pairs:

IFAPPEND(l1, l2, false) -> APPEND(tl(l1), l2)
APPEND(l1, l2) -> IFAPPEND(l1, l2, is_empty(l1))

Rules:

is_empty(nil) -> true
is_empty(cons(x, l)) -> false
hd(cons(x, l)) -> x
tl(cons(x, l)) -> l
append(l1, l2) -> ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) -> l2
ifappend(l1, l2, false) -> cons(hd(l1), append(tl(l1), l2))

Strategy:

innermost

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

     ↳DPs

       →DP Problem 1

         ↳UsableRules

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pairs:

IFAPPEND(l1, l2, false) -> APPEND(tl(l1), l2)
APPEND(l1, l2) -> IFAPPEND(l1, l2, is_empty(l1))

Rules:

tl(cons(x, l)) -> l
is_empty(cons(x, l)) -> false
is_empty(nil) -> true

Strategy:

innermost

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

APPEND(l1, l2) -> IFAPPEND(l1, l2, is_empty(l1))

two new Dependency Pairs are created:

APPEND(cons(x', l'), l2) -> IFAPPEND(cons(x', l'), l2, false)
APPEND(nil, l2) -> IFAPPEND(nil, l2, true)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳UsableRules

           →DP Problem 2

             ↳Nar

...

               →DP Problem 3

                 ↳Narrowing Transformation

Dependency Pairs:

APPEND(cons(x', l'), l2) -> IFAPPEND(cons(x', l'), l2, false)
IFAPPEND(l1, l2, false) -> APPEND(tl(l1), l2)

Rules:

tl(cons(x, l)) -> l
is_empty(cons(x, l)) -> false
is_empty(nil) -> true

Strategy:

innermost

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

IFAPPEND(l1, l2, false) -> APPEND(tl(l1), l2)

one new Dependency Pair is created:

IFAPPEND(cons(x', l'), l2, false) -> APPEND(l', l2)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳UsableRules

           →DP Problem 2

             ↳Nar

...

               →DP Problem 4

                 ↳Usable Rules (Innermost)

Dependency Pairs:

IFAPPEND(cons(x', l'), l2, false) -> APPEND(l', l2)
APPEND(cons(x', l'), l2) -> IFAPPEND(cons(x', l'), l2, false)

Rules:

tl(cons(x, l)) -> l
is_empty(cons(x, l)) -> false
is_empty(nil) -> true

Strategy:

innermost

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

     ↳DPs

       →DP Problem 1

         ↳UsableRules

           →DP Problem 2

             ↳Nar

...

               →DP Problem 5

                 ↳Size-Change Principle

Dependency Pairs:

IFAPPEND(cons(x', l'), l2, false) -> APPEND(l', l2)
APPEND(cons(x', l'), l2) -> IFAPPEND(cons(x', l'), l2, false)

Rule:

none

Strategy:

innermost

We number the DPs as follows:

IFAPPEND(cons(x', l'), l2, false) -> APPEND(l', l2)
APPEND(cons(x', l'), l2) -> IFAPPEND(cons(x', l'), l2, false)

and get the following Size-Change Graph(s):

{1}	,	{1}
1	>	1
2	=	2

{2}	,	{2}
1	=	1
2	=	2

which lead(s) to this/these maximal multigraph(s):

{1}	,	{2}
1	>	1
2	=	2

{2}	,	{1}
1	>	1
2	=	2

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.

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