Termination Proof using AProVE

Term Rewriting System R:
[f, x, h, t]
app(app(twice, f), x) -> app(f, app(f, x))
app(app(map, f), nil) -> nil
app(app(map, f), app(app(cons, h), t)) -> app(app(cons, app(f, h)), app(app(map, f), t))
app(app(fmap, nil), x) -> nil
app(app(fmap, app(app(cons, f), t_f)), x) -> app(app(cons, app(f, x)), app(app(fmap, t_f), x))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

APP(app(twice, f), x) -> APP(f, app(f, x))
APP(app(twice, f), x) -> APP(f, x)
APP(app(map, f), app(app(cons, h), t)) -> APP(app(cons, app(f, h)), app(app(map, f), t))
APP(app(map, f), app(app(cons, h), t)) -> APP(cons, app(f, h))
APP(app(map, f), app(app(cons, h), t)) -> APP(f, h)
APP(app(map, f), app(app(cons, h), t)) -> APP(app(map, f), t)
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(app(cons, app(f, x)), app(app(fmap, t_f), x))
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(cons, app(f, x))
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(f, x)
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(app(fmap, t_f), x)
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(fmap, t_f)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Narrowing Transformation

Dependency Pairs:

APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(app(fmap, t_f), x)
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(f, x)
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(app(cons, app(f, x)), app(app(fmap, t_f), x))
APP(app(map, f), app(app(cons, h), t)) -> APP(app(map, f), t)
APP(app(map, f), app(app(cons, h), t)) -> APP(f, h)
APP(app(map, f), app(app(cons, h), t)) -> APP(app(cons, app(f, h)), app(app(map, f), t))
APP(app(twice, f), x) -> APP(f, x)
APP(app(twice, f), x) -> APP(f, app(f, x))

Rules:

app(app(twice, f), x) -> app(f, app(f, x))
app(app(map, f), nil) -> nil
app(app(map, f), app(app(cons, h), t)) -> app(app(cons, app(f, h)), app(app(map, f), t))
app(app(fmap, nil), x) -> nil
app(app(fmap, app(app(cons, f), t_f)), x) -> app(app(cons, app(f, x)), app(app(fmap, t_f), x))

Strategy:

innermost

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

APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(app(fmap, t_f), x)

no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pairs:

APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(app(cons, app(f, x)), app(app(fmap, t_f), x))
APP(app(map, f), app(app(cons, h), t)) -> APP(app(map, f), t)
APP(app(map, f), app(app(cons, h), t)) -> APP(f, h)
APP(app(map, f), app(app(cons, h), t)) -> APP(app(cons, app(f, h)), app(app(map, f), t))
APP(app(twice, f), x) -> APP(f, x)
APP(app(twice, f), x) -> APP(f, app(f, x))
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(f, x)

Rules:

app(app(twice, f), x) -> app(f, app(f, x))
app(app(map, f), nil) -> nil
app(app(map, f), app(app(cons, h), t)) -> app(app(cons, app(f, h)), app(app(map, f), t))
app(app(fmap, nil), x) -> nil
app(app(fmap, app(app(cons, f), t_f)), x) -> app(app(cons, app(f, x)), app(app(fmap, t_f), x))

Strategy:

innermost

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

APP(app(twice, f), x) -> APP(f, app(f, x))

five new Dependency Pairs are created:

APP(app(twice, app(twice, f'')), x'') -> APP(app(twice, f''), app(f'', app(f'', x'')))
APP(app(twice, app(map, f'')), nil) -> APP(app(map, f''), nil)
APP(app(twice, app(map, f'')), app(app(cons, h'), t')) -> APP(app(map, f''), app(app(cons, app(f'', h')), app(app(map, f''), t')))
APP(app(twice, app(fmap, nil)), x'') -> APP(app(fmap, nil), nil)
APP(app(twice, app(fmap, app(app(cons, f''), t_f))), x'') -> APP(app(fmap, app(app(cons, f''), t_f)), app(app(cons, app(f'', x'')), app(app(fmap, t_f), x'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 3

                 ↳Narrowing Transformation

Dependency Pairs:

APP(app(twice, app(fmap, app(app(cons, f''), t_f))), x'') -> APP(app(fmap, app(app(cons, f''), t_f)), app(app(cons, app(f'', x'')), app(app(fmap, t_f), x'')))
APP(app(twice, app(map, f'')), app(app(cons, h'), t')) -> APP(app(map, f''), app(app(cons, app(f'', h')), app(app(map, f''), t')))
APP(app(twice, app(twice, f'')), x'') -> APP(app(twice, f''), app(f'', app(f'', x'')))
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(f, x)
APP(app(map, f), app(app(cons, h), t)) -> APP(app(map, f), t)
APP(app(map, f), app(app(cons, h), t)) -> APP(f, h)
APP(app(map, f), app(app(cons, h), t)) -> APP(app(cons, app(f, h)), app(app(map, f), t))
APP(app(twice, f), x) -> APP(f, x)
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(app(cons, app(f, x)), app(app(fmap, t_f), x))

Rules:

app(app(twice, f), x) -> app(f, app(f, x))
app(app(map, f), nil) -> nil
app(app(map, f), app(app(cons, h), t)) -> app(app(cons, app(f, h)), app(app(map, f), t))
app(app(fmap, nil), x) -> nil
app(app(fmap, app(app(cons, f), t_f)), x) -> app(app(cons, app(f, x)), app(app(fmap, t_f), x))

Strategy:

innermost

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

APP(app(map, f), app(app(cons, h), t)) -> APP(app(cons, app(f, h)), app(app(map, f), t))

seven new Dependency Pairs are created:

APP(app(map, app(twice, f'')), app(app(cons, h'), t)) -> APP(app(cons, app(f'', app(f'', h'))), app(app(map, app(twice, f'')), t))
APP(app(map, app(map, f'')), app(app(cons, nil), t)) -> APP(app(cons, nil), app(app(map, app(map, f'')), t))
APP(app(map, app(map, f'')), app(app(cons, app(app(cons, h''), t'')), t)) -> APP(app(cons, app(app(cons, app(f'', h'')), app(app(map, f''), t''))), app(app(map, app(map, f'')), t))
APP(app(map, app(fmap, nil)), app(app(cons, h'), t)) -> APP(app(cons, nil), app(app(map, app(fmap, nil)), t))
APP(app(map, app(fmap, app(app(cons, f''), t_f))), app(app(cons, h'), t)) -> APP(app(cons, app(app(cons, app(f'', h')), app(app(fmap, t_f), h'))), app(app(map, app(fmap, app(app(cons, f''), t_f))), t))
APP(app(map, f''), app(app(cons, h), nil)) -> APP(app(cons, app(f'', h)), nil)
APP(app(map, f''), app(app(cons, h), app(app(cons, h''), t''))) -> APP(app(cons, app(f'', h)), app(app(cons, app(f'', h'')), app(app(map, f''), t'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 4

                 ↳Narrowing Transformation

Dependency Pairs:

APP(app(map, f''), app(app(cons, h), app(app(cons, h''), t''))) -> APP(app(cons, app(f'', h)), app(app(cons, app(f'', h'')), app(app(map, f''), t'')))
APP(app(map, f''), app(app(cons, h), nil)) -> APP(app(cons, app(f'', h)), nil)
APP(app(map, app(fmap, app(app(cons, f''), t_f))), app(app(cons, h'), t)) -> APP(app(cons, app(app(cons, app(f'', h')), app(app(fmap, t_f), h'))), app(app(map, app(fmap, app(app(cons, f''), t_f))), t))
APP(app(map, app(fmap, nil)), app(app(cons, h'), t)) -> APP(app(cons, nil), app(app(map, app(fmap, nil)), t))
APP(app(map, app(map, f'')), app(app(cons, app(app(cons, h''), t'')), t)) -> APP(app(cons, app(app(cons, app(f'', h'')), app(app(map, f''), t''))), app(app(map, app(map, f'')), t))
APP(app(twice, app(map, f'')), app(app(cons, h'), t')) -> APP(app(map, f''), app(app(cons, app(f'', h')), app(app(map, f''), t')))
APP(app(twice, app(twice, f'')), x'') -> APP(app(twice, f''), app(f'', app(f'', x'')))
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(f, x)
APP(app(map, app(twice, f'')), app(app(cons, h'), t)) -> APP(app(cons, app(f'', app(f'', h'))), app(app(map, app(twice, f'')), t))
APP(app(map, f), app(app(cons, h), t)) -> APP(app(map, f), t)
APP(app(map, f), app(app(cons, h), t)) -> APP(f, h)
APP(app(twice, f), x) -> APP(f, x)
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(app(cons, app(f, x)), app(app(fmap, t_f), x))
APP(app(twice, app(fmap, app(app(cons, f''), t_f))), x'') -> APP(app(fmap, app(app(cons, f''), t_f)), app(app(cons, app(f'', x'')), app(app(fmap, t_f), x'')))

Rules:

app(app(twice, f), x) -> app(f, app(f, x))
app(app(map, f), nil) -> nil
app(app(map, f), app(app(cons, h), t)) -> app(app(cons, app(f, h)), app(app(map, f), t))
app(app(fmap, nil), x) -> nil
app(app(fmap, app(app(cons, f), t_f)), x) -> app(app(cons, app(f, x)), app(app(fmap, t_f), x))

Strategy:

innermost

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

APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(app(cons, app(f, x)), app(app(fmap, t_f), x))

five new Dependency Pairs are created:

APP(app(fmap, app(app(cons, app(twice, f'')), t_f)), x'') -> APP(app(cons, app(f'', app(f'', x''))), app(app(fmap, t_f), x''))
APP(app(fmap, app(app(cons, app(map, f'')), t_f)), nil) -> APP(app(cons, nil), app(app(fmap, t_f), nil))
APP(app(fmap, app(app(cons, app(map, f'')), t_f)), app(app(cons, h'), t')) -> APP(app(cons, app(app(cons, app(f'', h')), app(app(map, f''), t'))), app(app(fmap, t_f), app(app(cons, h'), t')))
APP(app(fmap, app(app(cons, app(fmap, nil)), t_f)), x'') -> APP(app(cons, nil), app(app(fmap, t_f), x''))
APP(app(fmap, app(app(cons, app(fmap, app(app(cons, f''), t_f))), t_f)), x'') -> APP(app(cons, app(app(cons, app(f'', x'')), app(app(fmap, t_f), x''))), app(app(fmap, t_f), x''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 5

                 ↳Narrowing Transformation

Dependency Pairs:

APP(app(fmap, app(app(cons, app(fmap, app(app(cons, f''), t_f))), t_f)), x'') -> APP(app(cons, app(app(cons, app(f'', x'')), app(app(fmap, t_f), x''))), app(app(fmap, t_f), x''))
APP(app(fmap, app(app(cons, app(fmap, nil)), t_f)), x'') -> APP(app(cons, nil), app(app(fmap, t_f), x''))
APP(app(fmap, app(app(cons, app(map, f'')), t_f)), app(app(cons, h'), t')) -> APP(app(cons, app(app(cons, app(f'', h')), app(app(map, f''), t'))), app(app(fmap, t_f), app(app(cons, h'), t')))
APP(app(fmap, app(app(cons, app(map, f'')), t_f)), nil) -> APP(app(cons, nil), app(app(fmap, t_f), nil))
APP(app(map, f''), app(app(cons, h), nil)) -> APP(app(cons, app(f'', h)), nil)
APP(app(map, app(fmap, app(app(cons, f''), t_f))), app(app(cons, h'), t)) -> APP(app(cons, app(app(cons, app(f'', h')), app(app(fmap, t_f), h'))), app(app(map, app(fmap, app(app(cons, f''), t_f))), t))
APP(app(map, app(fmap, nil)), app(app(cons, h'), t)) -> APP(app(cons, nil), app(app(map, app(fmap, nil)), t))
APP(app(fmap, app(app(cons, app(twice, f'')), t_f)), x'') -> APP(app(cons, app(f'', app(f'', x''))), app(app(fmap, t_f), x''))
APP(app(twice, app(fmap, app(app(cons, f''), t_f))), x'') -> APP(app(fmap, app(app(cons, f''), t_f)), app(app(cons, app(f'', x'')), app(app(fmap, t_f), x'')))
APP(app(map, app(map, f'')), app(app(cons, app(app(cons, h''), t'')), t)) -> APP(app(cons, app(app(cons, app(f'', h'')), app(app(map, f''), t''))), app(app(map, app(map, f'')), t))
APP(app(twice, app(map, f'')), app(app(cons, h'), t')) -> APP(app(map, f''), app(app(cons, app(f'', h')), app(app(map, f''), t')))
APP(app(twice, app(twice, f'')), x'') -> APP(app(twice, f''), app(f'', app(f'', x'')))
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(f, x)
APP(app(map, app(twice, f'')), app(app(cons, h'), t)) -> APP(app(cons, app(f'', app(f'', h'))), app(app(map, app(twice, f'')), t))
APP(app(map, f), app(app(cons, h), t)) -> APP(app(map, f), t)
APP(app(map, f), app(app(cons, h), t)) -> APP(f, h)
APP(app(twice, f), x) -> APP(f, x)
APP(app(map, f''), app(app(cons, h), app(app(cons, h''), t''))) -> APP(app(cons, app(f'', h)), app(app(cons, app(f'', h'')), app(app(map, f''), t'')))

Rules:

app(app(twice, f), x) -> app(f, app(f, x))
app(app(map, f), nil) -> nil
app(app(map, f), app(app(cons, h), t)) -> app(app(cons, app(f, h)), app(app(map, f), t))
app(app(fmap, nil), x) -> nil
app(app(fmap, app(app(cons, f), t_f)), x) -> app(app(cons, app(f, x)), app(app(fmap, t_f), x))

Strategy:

innermost

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

APP(app(fmap, app(app(cons, app(map, f'')), t_f)), nil) -> APP(app(cons, nil), app(app(fmap, t_f), nil))

no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 6

                 ↳Narrowing Transformation

Dependency Pairs:

APP(app(fmap, app(app(cons, app(map, f'')), t_f)), app(app(cons, h'), t')) -> APP(app(cons, app(app(cons, app(f'', h')), app(app(map, f''), t'))), app(app(fmap, t_f), app(app(cons, h'), t')))
APP(app(map, f''), app(app(cons, h), app(app(cons, h''), t''))) -> APP(app(cons, app(f'', h)), app(app(cons, app(f'', h'')), app(app(map, f''), t'')))
APP(app(fmap, app(app(cons, app(fmap, nil)), t_f)), x'') -> APP(app(cons, nil), app(app(fmap, t_f), x''))
APP(app(map, f''), app(app(cons, h), nil)) -> APP(app(cons, app(f'', h)), nil)
APP(app(map, app(fmap, app(app(cons, f''), t_f))), app(app(cons, h'), t)) -> APP(app(cons, app(app(cons, app(f'', h')), app(app(fmap, t_f), h'))), app(app(map, app(fmap, app(app(cons, f''), t_f))), t))
APP(app(map, app(fmap, nil)), app(app(cons, h'), t)) -> APP(app(cons, nil), app(app(map, app(fmap, nil)), t))
APP(app(fmap, app(app(cons, app(twice, f'')), t_f)), x'') -> APP(app(cons, app(f'', app(f'', x''))), app(app(fmap, t_f), x''))
APP(app(twice, app(fmap, app(app(cons, f''), t_f))), x'') -> APP(app(fmap, app(app(cons, f''), t_f)), app(app(cons, app(f'', x'')), app(app(fmap, t_f), x'')))
APP(app(map, app(map, f'')), app(app(cons, app(app(cons, h''), t'')), t)) -> APP(app(cons, app(app(cons, app(f'', h'')), app(app(map, f''), t''))), app(app(map, app(map, f'')), t))
APP(app(twice, app(map, f'')), app(app(cons, h'), t')) -> APP(app(map, f''), app(app(cons, app(f'', h')), app(app(map, f''), t')))
APP(app(twice, app(twice, f'')), x'') -> APP(app(twice, f''), app(f'', app(f'', x'')))
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(f, x)
APP(app(map, app(twice, f'')), app(app(cons, h'), t)) -> APP(app(cons, app(f'', app(f'', h'))), app(app(map, app(twice, f'')), t))
APP(app(map, f), app(app(cons, h), t)) -> APP(app(map, f), t)
APP(app(map, f), app(app(cons, h), t)) -> APP(f, h)
APP(app(twice, f), x) -> APP(f, x)
APP(app(fmap, app(app(cons, app(fmap, app(app(cons, f''), t_f))), t_f)), x'') -> APP(app(cons, app(app(cons, app(f'', x'')), app(app(fmap, t_f), x''))), app(app(fmap, t_f), x''))

Rules:

app(app(twice, f), x) -> app(f, app(f, x))
app(app(map, f), nil) -> nil
app(app(map, f), app(app(cons, h), t)) -> app(app(cons, app(f, h)), app(app(map, f), t))
app(app(fmap, nil), x) -> nil
app(app(fmap, app(app(cons, f), t_f)), x) -> app(app(cons, app(f, x)), app(app(fmap, t_f), x))

Strategy:

innermost

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

APP(app(fmap, app(app(cons, app(fmap, nil)), t_f)), x'') -> APP(app(cons, nil), app(app(fmap, t_f), x''))

no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 7

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

APP(app(map, f''), app(app(cons, h), app(app(cons, h''), t''))) -> APP(app(cons, app(f'', h)), app(app(cons, app(f'', h'')), app(app(map, f''), t'')))
APP(app(fmap, app(app(cons, app(fmap, app(app(cons, f''), t_f))), t_f)), x'') -> APP(app(cons, app(app(cons, app(f'', x'')), app(app(fmap, t_f), x''))), app(app(fmap, t_f), x''))
APP(app(map, f''), app(app(cons, h), nil)) -> APP(app(cons, app(f'', h)), nil)
APP(app(map, app(fmap, app(app(cons, f''), t_f))), app(app(cons, h'), t)) -> APP(app(cons, app(app(cons, app(f'', h')), app(app(fmap, t_f), h'))), app(app(map, app(fmap, app(app(cons, f''), t_f))), t))
APP(app(map, app(fmap, nil)), app(app(cons, h'), t)) -> APP(app(cons, nil), app(app(map, app(fmap, nil)), t))
APP(app(fmap, app(app(cons, app(twice, f'')), t_f)), x'') -> APP(app(cons, app(f'', app(f'', x''))), app(app(fmap, t_f), x''))
APP(app(twice, app(fmap, app(app(cons, f''), t_f))), x'') -> APP(app(fmap, app(app(cons, f''), t_f)), app(app(cons, app(f'', x'')), app(app(fmap, t_f), x'')))
APP(app(map, app(map, f'')), app(app(cons, app(app(cons, h''), t'')), t)) -> APP(app(cons, app(app(cons, app(f'', h'')), app(app(map, f''), t''))), app(app(map, app(map, f'')), t))
APP(app(twice, app(map, f'')), app(app(cons, h'), t')) -> APP(app(map, f''), app(app(cons, app(f'', h')), app(app(map, f''), t')))
APP(app(twice, app(twice, f'')), x'') -> APP(app(twice, f''), app(f'', app(f'', x'')))
APP(app(fmap, app(app(cons, f), t_f)), x) -> APP(f, x)
APP(app(map, app(twice, f'')), app(app(cons, h'), t)) -> APP(app(cons, app(f'', app(f'', h'))), app(app(map, app(twice, f'')), t))
APP(app(map, f), app(app(cons, h), t)) -> APP(app(map, f), t)
APP(app(map, f), app(app(cons, h), t)) -> APP(f, h)
APP(app(twice, f), x) -> APP(f, x)
APP(app(fmap, app(app(cons, app(map, f'')), t_f)), app(app(cons, h'), t')) -> APP(app(cons, app(app(cons, app(f'', h')), app(app(map, f''), t'))), app(app(fmap, t_f), app(app(cons, h'), t')))

Rules:

app(app(twice, f), x) -> app(f, app(f, x))
app(app(map, f), nil) -> nil
app(app(map, f), app(app(cons, h), t)) -> app(app(cons, app(f, h)), app(app(map, f), t))
app(app(fmap, nil), x) -> nil
app(app(fmap, app(app(cons, f), t_f)), x) -> app(app(cons, app(f, x)), app(app(fmap, t_f), x))

Strategy:

innermost

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