Term Rewriting System R:
[ys, x, xs, f]
app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))

Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(cons, x), app(app(append, xs), ys))
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(append, xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(app(cons, app(f, x)), nil)
APP(app(flatwith, f), app(leaf, x)) -> APP(cons, app(f, x))
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(node, xs)) -> APP(flatwithsub, f)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(append, app(app(flatwith, f), x))
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(flatwith, f)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)

Furthermore, R contains one SCC.


   R
DPs
       →DP Problem 1
Narrowing Transformation


Dependency Pairs:

APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(flatwith, f), app(leaf, x)) -> APP(app(cons, app(f, x)), nil)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(cons, x), app(app(append, xs), ys))


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(cons, x), app(app(append, xs), ys))
two new Dependency Pairs are created:

APP(app(append, app(app(cons, x), nil)), ys'') -> APP(app(cons, x), ys'')
APP(app(append, app(app(cons, x), app(app(cons, x''), xs''))), ys'') -> APP(app(cons, x), app(app(cons, x''), app(app(append, xs''), ys'')))

The transformation is resulting in one new DP problem:



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


Dependency Pairs:

APP(app(append, app(app(cons, x), app(app(cons, x''), xs''))), ys'') -> APP(app(cons, x), app(app(cons, x''), app(app(append, xs''), ys'')))
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), nil)), ys'') -> APP(app(cons, x), ys'')
APP(app(flatwith, f), app(leaf, x)) -> APP(app(cons, app(f, x)), nil)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, f), app(leaf, x)) -> APP(app(cons, app(f, x)), nil)
six new Dependency Pairs are created:

APP(app(flatwith, app(append, nil)), app(leaf, x')) -> APP(app(cons, x'), nil)
APP(app(flatwith, app(append, app(app(cons, x''), xs'))), app(leaf, x0)) -> APP(app(cons, app(app(cons, x''), app(app(append, xs'), x0))), nil)
APP(app(flatwith, app(flatwith, f'')), app(leaf, app(leaf, x''))) -> APP(app(cons, app(app(cons, app(f'', x'')), nil)), nil)
APP(app(flatwith, app(flatwith, f'')), app(leaf, app(node, xs'))) -> APP(app(cons, app(app(flatwithsub, f''), xs')), nil)
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, nil)) -> APP(app(cons, nil), nil)
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)

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(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, nil)) -> APP(app(cons, nil), nil)
APP(app(flatwith, app(flatwith, f'')), app(leaf, app(node, xs'))) -> APP(app(cons, app(app(flatwithsub, f''), xs')), nil)
APP(app(flatwith, app(flatwith, f'')), app(leaf, app(leaf, x''))) -> APP(app(cons, app(app(cons, app(f'', x'')), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), xs'))), app(leaf, x0)) -> APP(app(cons, app(app(cons, x''), app(app(append, xs'), x0))), nil)
APP(app(flatwith, app(append, nil)), app(leaf, x')) -> APP(app(cons, x'), nil)
APP(app(append, app(app(cons, x), nil)), ys'') -> APP(app(cons, x), ys'')
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(append, app(app(cons, x), app(app(cons, x''), xs''))), ys'') -> APP(app(cons, x), app(app(cons, x''), app(app(append, xs''), ys'')))


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(append, app(app(cons, x), nil)), ys'') -> APP(app(cons, x), ys'')
no new Dependency Pairs are created.
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(flatwith, app(flatwithsub, f'')), app(leaf, nil)) -> APP(app(cons, nil), nil)
APP(app(flatwith, app(flatwith, f'')), app(leaf, app(node, xs'))) -> APP(app(cons, app(app(flatwithsub, f''), xs')), nil)
APP(app(flatwith, app(flatwith, f'')), app(leaf, app(leaf, x''))) -> APP(app(cons, app(app(cons, app(f'', x'')), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), xs'))), app(leaf, x0)) -> APP(app(cons, app(app(cons, x''), app(app(append, xs'), x0))), nil)
APP(app(flatwith, app(append, nil)), app(leaf, x')) -> APP(app(cons, x'), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), xs''))), ys'') -> APP(app(cons, x), app(app(cons, x''), app(app(append, xs''), ys'')))
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(append, app(app(cons, x), app(app(cons, x''), xs''))), ys'') -> APP(app(cons, x), app(app(cons, x''), app(app(append, xs''), ys'')))
two new Dependency Pairs are created:

APP(app(append, app(app(cons, x), app(app(cons, x''), nil))), ys''') -> APP(app(cons, x), app(app(cons, x''), ys'''))
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), xs')))), ys''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(append, xs'), ys'''))))

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(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwith, app(flatwith, f'')), app(leaf, app(node, xs'))) -> APP(app(cons, app(app(flatwithsub, f''), xs')), nil)
APP(app(flatwith, app(flatwith, f'')), app(leaf, app(leaf, x''))) -> APP(app(cons, app(app(cons, app(f'', x'')), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), xs')))), ys''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(append, xs'), ys'''))))
APP(app(flatwith, app(append, app(app(cons, x''), xs'))), app(leaf, x0)) -> APP(app(cons, app(app(cons, x''), app(app(append, xs'), x0))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), nil))), ys''') -> APP(app(cons, x), app(app(cons, x''), ys'''))
APP(app(flatwith, app(append, nil)), app(leaf, x')) -> APP(app(cons, x'), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, nil)) -> APP(app(cons, nil), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(append, nil)), app(leaf, x')) -> APP(app(cons, x'), nil)
no new Dependency Pairs are created.
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(flatwith, app(flatwithsub, f'')), app(leaf, nil)) -> APP(app(cons, nil), nil)
APP(app(flatwith, app(flatwith, f'')), app(leaf, app(node, xs'))) -> APP(app(cons, app(app(flatwithsub, f''), xs')), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), xs')))), ys''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(append, xs'), ys'''))))
APP(app(flatwith, app(flatwith, f'')), app(leaf, app(leaf, x''))) -> APP(app(cons, app(app(cons, app(f'', x'')), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), nil))), ys''') -> APP(app(cons, x), app(app(cons, x''), ys'''))
APP(app(flatwith, app(append, app(app(cons, x''), xs'))), app(leaf, x0)) -> APP(app(cons, app(app(cons, x''), app(app(append, xs'), x0))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(append, app(app(cons, x''), xs'))), app(leaf, x0)) -> APP(app(cons, app(app(cons, x''), app(app(append, xs'), x0))), nil)
two new Dependency Pairs are created:

APP(app(flatwith, app(append, app(app(cons, x''), nil))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), x0')), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), xs'')))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(append, xs''), x0')))), nil)

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(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), xs'')))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(append, xs''), x0')))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), nil))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), x0')), nil)
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), xs')))), ys''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(append, xs'), ys'''))))
APP(app(flatwith, app(flatwith, f'')), app(leaf, app(node, xs'))) -> APP(app(cons, app(app(flatwithsub, f''), xs')), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), nil))), ys''') -> APP(app(cons, x), app(app(cons, x''), ys'''))
APP(app(flatwith, app(flatwith, f'')), app(leaf, app(leaf, x''))) -> APP(app(cons, app(app(cons, app(f'', x'')), nil)), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, nil)) -> APP(app(cons, nil), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, f'')), app(leaf, app(leaf, x''))) -> APP(app(cons, app(app(cons, app(f'', x'')), nil)), nil)
six new Dependency Pairs are created:

APP(app(flatwith, app(flatwith, app(append, nil))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, x'''), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(leaf, x')))) -> APP(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, nil))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), 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(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, nil))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(leaf, x')))) -> APP(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, nil))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, x'''), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), nil))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), x0')), nil)
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), xs')))), ys''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(append, xs'), ys'''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, nil)) -> APP(app(cons, nil), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), nil))), ys''') -> APP(app(cons, x), app(app(cons, x''), ys'''))
APP(app(flatwith, app(flatwith, f'')), app(leaf, app(node, xs'))) -> APP(app(cons, app(app(flatwithsub, f''), xs')), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), xs'')))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(append, xs''), x0')))), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, f'')), app(leaf, app(node, xs'))) -> APP(app(cons, app(app(flatwithsub, f''), xs')), nil)
two new Dependency Pairs are created:

APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, nil))) -> APP(app(cons, nil), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 9
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, nil))) -> APP(app(cons, nil), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, nil))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(leaf, x')))) -> APP(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, nil))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, x'''), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), xs'')))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(append, xs''), x0')))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), nil))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), x0')), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), xs')))), ys''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(append, xs'), ys'''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), nil))), ys''') -> APP(app(cons, x), app(app(cons, x''), ys'''))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, nil)) -> APP(app(cons, nil), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwithsub, f'')), app(leaf, nil)) -> APP(app(cons, nil), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 10
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, nil))) -> APP(app(cons, nil), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, nil))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(leaf, x')))) -> APP(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, nil))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, x'''), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), xs'')))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(append, xs''), x0')))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), nil))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), x0')), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), xs')))), ys''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(append, xs'), ys'''))))
APP(app(append, app(app(cons, x), app(app(cons, x''), nil))), ys''') -> APP(app(cons, x), app(app(cons, x''), ys'''))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(append, app(app(cons, x), app(app(cons, x''), nil))), ys''') -> APP(app(cons, x), app(app(cons, x''), ys'''))
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 11
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, nil))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(leaf, x')))) -> APP(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, nil))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, x'''), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), xs'')))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(append, xs''), x0')))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), nil))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), x0')), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), xs')))), ys''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(append, xs'), ys'''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, nil))) -> APP(app(cons, nil), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(append, app(app(cons, x''), nil))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), x0')), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 12
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, nil))) -> APP(app(cons, nil), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, nil))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(leaf, x')))) -> APP(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, nil))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, x'''), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), xs'')))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(append, xs''), x0')))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), xs')))), ys''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(append, xs'), ys'''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(append, nil))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, x'''), nil)), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 13
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, nil))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(leaf, x')))) -> APP(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), xs'')))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(append, xs''), x0')))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), xs')))), ys''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(append, xs'), ys'''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, nil))) -> APP(app(cons, nil), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, nil))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 14
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, nil))) -> APP(app(cons, nil), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(leaf, x')))) -> APP(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), xs'')))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(append, xs''), x0')))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), xs')))), ys''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(append, xs'), ys'''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, nil))) -> APP(app(cons, nil), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 15
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(leaf, x')))) -> APP(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), xs'')))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(append, xs''), x0')))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), xs')))), ys''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(append, xs'), ys'''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), xs')))), ys''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(append, xs'), ys'''))))
two new Dependency Pairs are created:

APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), nil)))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), ys'''')))
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), xs''))))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(append, xs''), ys'''')))))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 16
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(leaf, x')))) -> APP(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), xs''))))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(append, xs''), ys'''')))))
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), xs'')))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(append, xs''), x0')))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), nil)))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), ys'''')))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), xs'')))), app(leaf, x0')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(append, xs''), x0')))), nil)
two new Dependency Pairs are created:

APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), nil)))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), x0''))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), xs'))))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(append, xs'), x0''))))), nil)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 17
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), xs'))))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(append, xs'), x0''))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), nil)))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), x0''))), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(leaf, x')))) -> APP(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), xs''))))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(append, xs''), ys'''')))))
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), nil)))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), ys'''')))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))), app(leaf, app(leaf, x'''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)
two new Dependency Pairs are created:

APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), nil)))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), x'''')), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), xs''))))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(append, xs''), x'''')))), nil)), nil)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 18
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), xs''))))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(append, xs''), x'''')))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), nil)))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), x'''')), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), nil)))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), x0''))), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), xs''))))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(append, xs''), ys'''')))))
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(leaf, x')))) -> APP(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), nil)))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), ys'''')))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), xs'))))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(append, xs'), x0''))))), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(leaf, x')))) -> APP(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)
six new Dependency Pairs are created:

APP(app(flatwith, app(flatwith, app(flatwith, app(append, nil)))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, x''), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), xs'))))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(append, xs'), x''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(leaf, x''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f'', x'')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(node, xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f''), xs')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 19
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(node, xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f''), xs')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(leaf, x''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f'', x'')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), xs'))))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(append, xs'), x''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, nil)))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, x''), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), nil)))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), x'''')), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), xs'))))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(append, xs'), x0''))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), nil)))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), x0''))), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), xs''))))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(append, xs''), ys'''')))))
APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), nil)))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), ys'''')))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), xs''))))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(append, xs''), x'''')))), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(flatwith, f'))), app(leaf, app(leaf, app(node, xs')))) -> APP(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)
two new Dependency Pairs are created:

APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 20
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(node, xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f''), xs')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(leaf, x''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f'', x'')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), xs'))))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(append, xs'), x''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, nil)))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, x''), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), xs''))))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(append, xs''), x'''')))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), nil)))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), x'''')), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), xs'))))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(append, xs'), x0''))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), nil)))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), x0''))), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), xs''))))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(append, xs''), ys'''')))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), nil)))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), ys'''')))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), nil)))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), ys'''')))
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 21
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(node, xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f''), xs')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(leaf, x''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f'', x'')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), xs'))))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(append, xs'), x''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, nil)))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, x''), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), xs''))))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(append, xs''), x'''')))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), nil)))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), x'''')), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), xs'))))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(append, xs'), x0''))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), nil)))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), x0''))), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), xs''))))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(append, xs''), ys'''')))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), xs''))))), ys'''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(append, xs''), ys'''')))))
two new Dependency Pairs are created:

APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), nil))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), ys'''''))))
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 22
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(node, xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f''), xs')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(leaf, x''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f'', x'')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), xs'))))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(append, xs'), x''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, nil)))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, x''), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), xs''))))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(append, xs''), x'''')))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), nil)))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), x'''')), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), xs'))))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(append, xs'), x0''))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), nil)))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), x0''))), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), nil))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), ys'''''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), nil)))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), x0''))), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 23
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(node, xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f''), xs')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(leaf, x''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f'', x'')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), xs'))))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(append, xs'), x''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, nil)))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, x''), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), xs''))))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(append, xs''), x'''')))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), nil)))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), x'''')), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), xs'))))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(append, xs'), x0''))))), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), nil))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), ys'''''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), xs'))))), app(leaf, x0'')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(append, xs'), x0''))))), nil)
two new Dependency Pairs are created:

APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), nil))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), x0''')))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 24
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), nil))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), x0''')))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(node, xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f''), xs')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(leaf, x''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f'', x'')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), xs'))))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(append, xs'), x''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, nil)))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, x''), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), xs''))))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(append, xs''), x'''')))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), nil)))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), x'''')), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), nil))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), ys'''''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), nil)))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), x'''')), nil)), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 25
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), nil))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), x0''')))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(node, xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f''), xs')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(leaf, x''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f'', x'')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), xs'))))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(append, xs'), x''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, nil)))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, x''), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), xs''))))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(append, xs''), x'''')))), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), nil))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), ys'''''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), xs''))))), app(leaf, app(leaf, x''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(append, xs''), x'''')))), nil)), nil)
two new Dependency Pairs are created:

APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), nil))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), x'''''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 26
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), nil))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), x'''''))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(node, xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f''), xs')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(leaf, x''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f'', x'')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), xs'))))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(append, xs'), x''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, nil)))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, x''), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), nil))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), ys'''''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), nil))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), x0''')))), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(flatwith, app(append, nil)))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, x''), nil)), nil)), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 27
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), nil))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), x'''''))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), nil))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), x0''')))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(node, xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f''), xs')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(leaf, x''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f'', x'')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), xs'))))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(append, xs'), x''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), nil))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), ys'''''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), xs'))))), app(leaf, app(leaf, app(leaf, x'')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(append, xs'), x''))), nil)), nil)), nil)
two new Dependency Pairs are created:

APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), nil))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), x''')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), app(app(cons, x'), xs'')))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(cons, x'), app(app(append, xs''), x''')))), nil)), nil)), nil)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 28
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), app(app(cons, x'), xs'')))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(cons, x'), app(app(append, xs''), x''')))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), nil))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), x''')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), nil))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), x0''')))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(node, xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f''), xs')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(leaf, x''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f'', x'')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), nil))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), ys'''''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), nil))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), x'''''))), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(leaf, x''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f'', x'')), nil)), nil)), nil)), nil)
six new Dependency Pairs are created:

APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, nil))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x'''), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(leaf, x')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(node, xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(app(cons, x'), xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)), nil)), nil)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 29
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(app(cons, x'), xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(node, xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(leaf, x')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, nil))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x'''), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), nil))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), x''')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), nil))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), x'''''))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), nil))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), x0''')))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(node, xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f''), xs')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), nil))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), ys'''''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), app(app(cons, x'), xs'')))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(cons, x'), app(app(append, xs''), x''')))), nil)), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'')))), app(leaf, app(leaf, app(leaf, app(node, xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f''), xs')), nil)), nil)), nil)
two new Dependency Pairs are created:

APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, app(app(cons, x'), xs'')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)), nil)), nil)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 30
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, app(app(cons, x'), xs'')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(node, xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(leaf, x')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, nil))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x'''), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), app(app(cons, x'), xs'')))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(cons, x'), app(app(append, xs''), x''')))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), nil))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), x''')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), nil))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), x'''''))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), nil))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), x0''')))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), nil))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), ys'''''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(app(cons, x'), xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, nil)))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 31
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(app(cons, x'), xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(node, xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(leaf, x')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, nil))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x'''), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), app(app(cons, x'), xs'')))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(cons, x'), app(app(append, xs''), x''')))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), nil))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), x''')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), nil))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), x'''''))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), nil))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), x0''')))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), nil))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), ys'''''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, app(app(cons, x'), xs'')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, nil)))) -> APP(app(cons, app(app(cons, nil), nil)), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 32
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, app(app(cons, x'), xs'')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(app(cons, x'), xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(node, xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(leaf, x')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, nil))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x'''), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), app(app(cons, x'), xs'')))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(cons, x'), app(app(append, xs''), x''')))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), nil))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), x''')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), nil))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), x'''''))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), nil))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), x0''')))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), nil))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), ys'''''))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), nil))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), ys'''''))))
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 33
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(app(cons, x'), xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(node, xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(leaf, x')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, nil))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x'''), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), app(app(cons, x'), xs'')))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(cons, x'), app(app(append, xs''), x''')))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), nil))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), x''')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), nil))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), x'''''))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), nil))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), x0''')))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, app(app(cons, x'), xs'')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), xs')))))), ys''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(append, xs'), ys'''''))))))
two new Dependency Pairs are created:

APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), nil)))))), ys'''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), ys'''''')))))
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(cons, x'2), xs''))))))), ys'''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(cons, x'2), app(app(append, xs''), ys'''''')))))))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 34
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, app(app(cons, x'), xs'')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(app(cons, x'), xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(node, xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(leaf, x')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, nil))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x'''), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), app(app(cons, x'), xs'')))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(cons, x'), app(app(append, xs''), x''')))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), nil))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), x''')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), nil))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), x'''''))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), nil))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), x0''')))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(cons, x'2), xs''))))))), ys'''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(cons, x'2), app(app(append, xs''), ys'''''')))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), nil)))))), ys'''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), ys'''''')))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), nil))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), x0''')))), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 35
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(app(cons, x'), xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(node, xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(leaf, x')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, nil))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x'''), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), app(app(cons, x'), xs'')))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(cons, x'), app(app(append, xs''), x''')))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), nil))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), x''')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), nil))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), x'''''))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(cons, x'2), xs''))))))), ys'''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(cons, x'2), app(app(append, xs''), ys'''''')))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), nil)))))), ys'''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), ys'''''')))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, app(app(cons, x'), xs'')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), xs'')))))), app(leaf, x0''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x0''')))))), nil)
two new Dependency Pairs are created:

APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), nil)))))), app(leaf, x0'''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), x0''''))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(cons, x2), xs'))))))), app(leaf, x0'''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(cons, x2), app(app(append, xs'), x0''''))))))), nil)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 36
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(cons, x2), xs'))))))), app(leaf, x0'''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(cons, x2), app(app(append, xs'), x0''''))))))), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), nil)))))), app(leaf, x0'''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), x0''''))))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, app(app(cons, x'), xs'')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(app(cons, x'), xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(node, xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(leaf, x')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, nil))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x'''), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), app(app(cons, x'), xs'')))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(cons, x'), app(app(append, xs''), x''')))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), nil))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), x''')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), nil))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), x'''''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(cons, x'2), xs''))))))), ys'''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(cons, x'2), app(app(append, xs''), ys'''''')))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), nil)))))), ys'''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), ys'''''')))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), nil))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), x'''''))), nil)), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 37
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), nil)))))), app(leaf, x0'''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), x0''''))))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, app(app(cons, x'), xs'')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(app(cons, x'), xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(node, xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(leaf, x')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, nil))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x'''), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), app(app(cons, x'), xs'')))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(cons, x'), app(app(append, xs''), x''')))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), nil))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), x''')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(cons, x'2), xs''))))))), ys'''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), app(app(cons, x'2), app(app(append, xs''), ys'''''')))))))
APP(app(flatwith, app(flatwith, app(flatwithsub, f'))), app(leaf, app(leaf, app(app(cons, x'), xs')))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), nil)))))), ys'''''') -> APP(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), app(app(cons, x'1), ys'''''')))))
APP(app(flatwith, app(flatwithsub, f'')), app(leaf, app(app(cons, x''), xs'))) -> APP(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(flatwith, f), x)
APP(app(flatwithsub, f), app(app(cons, x), xs)) -> APP(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
APP(app(flatwith, f), app(node, xs)) -> APP(app(flatwithsub, f), xs)
APP(app(flatwith, f), app(leaf, x)) -> APP(f, x)
APP(app(append, app(app(cons, x), xs)), ys) -> APP(app(append, xs), ys)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(cons, x2), xs'))))))), app(leaf, x0'''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(cons, x2), app(app(append, xs'), x0''''))))))), nil)


Rules:


app(app(append, nil), ys) -> ys
app(app(append, app(app(cons, x), xs)), ys) -> app(app(cons, x), app(app(append, xs), ys))
app(app(flatwith, f), app(leaf, x)) -> app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) -> app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) -> nil
app(app(flatwithsub, f), app(app(cons, x), xs)) -> app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))





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

APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), xs')))))), app(leaf, app(leaf, x'''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(append, xs'), x'''''))))), nil)), nil)
two new Dependency Pairs are created:

APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), nil)))))), app(leaf, app(leaf, x''''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), x'''''')))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(cons, x1), xs''))))))), app(leaf, app(leaf, x''''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x'''''')))))), nil)), nil)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 38
Narrowing Transformation


Dependency Pairs:

APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(cons, x1), xs''))))))), app(leaf, app(leaf, x''''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), app(app(cons, x1), app(app(append, xs''), x'''''')))))), nil)), nil)
APP(app(flatwith, app(flatwith, app(append, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), nil)))))), app(leaf, app(leaf, x''''''))) -> APP(app(cons, app(app(cons, app(app(cons, x'), app(app(cons, x''), app(app(cons, x0), x'''''')))), nil)), nil)
APP(app(flatwith, app(append, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(cons, x2), xs'))))))), app(leaf, x0'''')) -> APP(app(cons, app(app(cons, x''), app(app(cons, x'), app(app(cons, x0), app(app(cons, x1), app(app(cons, x2), app(app(append, xs'), x0''''))))))), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, app(app(cons, x'), xs'')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, f''')))), app(leaf, app(leaf, app(leaf, app(node, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(app(cons, x'), xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f'), x')), app(app(flatwithsub, f'), xs'))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, nil))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, nil), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(node, xs')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(flatwithsub, f'), xs')), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(flatwith, f'))))), app(leaf, app(leaf, app(leaf, app(leaf, app(leaf, x')))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, app(f', x')), nil)), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x'), xs')))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, app(app(cons, x'), app(app(append, xs'), x'''))), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwith, app(append, nil))))), app(leaf, app(leaf, app(leaf, app(leaf, x'''))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x'''), nil)), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), app(app(cons, x'), xs'')))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), app(app(cons, x'), app(app(append, xs''), x''')))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(append, app(app(cons, x0), nil))))), app(leaf, app(leaf, app(leaf, x''')))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(cons, x0), x''')), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, f''))), app(leaf, app(leaf, app(node, app(app(cons, x'), xs''))))) -> APP(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x')), app(app(flatwithsub, f''), xs''))), nil)), nil)
APP(app(flatwith, app(flatwith, app(flatwith, app(flatwithsub, f'')))), app(leaf, app(leaf, app(leaf, app(app(cons, x''), xs'))))) -> APP(app(cons, app(app(cons, app(app(cons, app(app(append, app(app(flatwith, f''), x'')), app(app(flatwithsub, f''), xs'))), nil)), nil)), nil)
APP(app(flatwith, app(flatwith, f''')), app(leaf, app(node, app(app(cons, x'), xs'')))) -> APP(app(cons, app(app(append, app(app(flatwith, f'''), x')), app(app(flatwithsub, f'''), xs''))), nil)
APP(app(append, app(app(cons, x), app(app(cons, x''), app(app(cons, x'''), app(app(cons, x'0), <