R
↳Dependency Pair Analysis
CONCAT(cons(U, V), Y) -> CONCAT(V, Y)
LESSLEAVES(cons(U, V), cons(W, Z)) -> LESSLEAVES(concat(U, V), concat(W, Z))
LESSLEAVES(cons(U, V), cons(W, Z)) -> CONCAT(U, V)
LESSLEAVES(cons(U, V), cons(W, Z)) -> CONCAT(W, Z)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳Nar
CONCAT(cons(U, V), Y) -> CONCAT(V, Y)
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
CONCAT(cons(U, V), Y) -> CONCAT(V, Y)
CONCAT(x1, x2) -> CONCAT(x1, x2)
cons(x1, x2) -> cons(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳Nar
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Narrowing Transformation
LESSLEAVES(cons(U, V), cons(W, Z)) -> LESSLEAVES(concat(U, V), concat(W, Z))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
four new Dependency Pairs are created:
LESSLEAVES(cons(U, V), cons(W, Z)) -> LESSLEAVES(concat(U, V), concat(W, Z))
LESSLEAVES(cons(leaf, V'), cons(W, Z)) -> LESSLEAVES(V', concat(W, Z))
LESSLEAVES(cons(cons(U'', V''), V0), cons(W, Z)) -> LESSLEAVES(cons(U'', concat(V'', V0)), concat(W, Z))
LESSLEAVES(cons(U, V), cons(leaf, Z')) -> LESSLEAVES(concat(U, V), Z')
LESSLEAVES(cons(U, V), cons(cons(U'', V''), Z')) -> LESSLEAVES(concat(U, V), cons(U'', concat(V'', Z')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Narrowing Transformation
LESSLEAVES(cons(U, V), cons(cons(U'', V''), Z')) -> LESSLEAVES(concat(U, V), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(U, V), cons(leaf, Z')) -> LESSLEAVES(concat(U, V), Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(W, Z)) -> LESSLEAVES(cons(U'', concat(V'', V0)), concat(W, Z))
LESSLEAVES(cons(leaf, V'), cons(W, Z)) -> LESSLEAVES(V', concat(W, Z))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
two new Dependency Pairs are created:
LESSLEAVES(cons(leaf, V'), cons(W, Z)) -> LESSLEAVES(V', concat(W, Z))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 5
↳Narrowing Transformation
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(U, V), cons(leaf, Z')) -> LESSLEAVES(concat(U, V), Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(W, Z)) -> LESSLEAVES(cons(U'', concat(V'', V0)), concat(W, Z))
LESSLEAVES(cons(U, V), cons(cons(U'', V''), Z')) -> LESSLEAVES(concat(U, V), cons(U'', concat(V'', Z')))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
four new Dependency Pairs are created:
LESSLEAVES(cons(cons(U'', V''), V0), cons(W, Z)) -> LESSLEAVES(cons(U'', concat(V'', V0)), concat(W, Z))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(W, Z)) -> LESSLEAVES(cons(U'', V0'), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), concat(W, Z))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 6
↳Narrowing Transformation
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), concat(W, Z))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(W, Z)) -> LESSLEAVES(cons(U'', V0'), concat(W, Z))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(U, V), cons(cons(U'', V''), Z')) -> LESSLEAVES(concat(U, V), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(U, V), cons(leaf, Z')) -> LESSLEAVES(concat(U, V), Z')
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
two new Dependency Pairs are created:
LESSLEAVES(cons(U, V), cons(leaf, Z')) -> LESSLEAVES(concat(U, V), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 7
↳Narrowing Transformation
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), concat(W, Z))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(W, Z)) -> LESSLEAVES(cons(U'', V0'), concat(W, Z))
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(U, V), cons(cons(U'', V''), Z')) -> LESSLEAVES(concat(U, V), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
four new Dependency Pairs are created:
LESSLEAVES(cons(U, V), cons(cons(U'', V''), Z')) -> LESSLEAVES(concat(U, V), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(U, V), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(concat(U, V), cons(U'', Z''))
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', concat(V''', Z''))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 8
↳Narrowing Transformation
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(U, V), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(concat(U, V), cons(U'', Z''))
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), concat(W, Z))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(W, Z)) -> LESSLEAVES(cons(U'', V0'), concat(W, Z))
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
two new Dependency Pairs are created:
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(W, Z)) -> LESSLEAVES(cons(U'', V0'), concat(W, Z))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', V0'), Z')
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', V0'), cons(U', concat(V', Z')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 9
↳Narrowing Transformation
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', V0'), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', V0'), Z')
LESSLEAVES(cons(U, V), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(concat(U, V), cons(U'', Z''))
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), concat(W, Z))
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', concat(V''', Z''))))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
four new Dependency Pairs are created:
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', V0'')), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), Z')
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(cons(U0, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), cons(U0, concat(V'', Z')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 10
↳Narrowing Transformation
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(cons(U0, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), cons(U0, concat(V'', Z')))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', V0'')), concat(W, Z))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', V0'), Z')
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(U, V), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(concat(U, V), cons(U'', Z''))
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', V0'), cons(U', concat(V', Z')))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
two new Dependency Pairs are created:
LESSLEAVES(cons(U, V), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(concat(U, V), cons(U'', Z''))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(V', cons(U'', Z''))
LESSLEAVES(cons(cons(U''', V''), V0), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(cons(U''', concat(V'', V0)), cons(U'', Z''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 11
↳Narrowing Transformation
LESSLEAVES(cons(cons(U''', V''), V0), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(cons(U''', concat(V'', V0)), cons(U'', Z''))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(V', cons(U'', Z''))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', V0'')), concat(W, Z))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', V0'), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', V0'), Z')
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(cons(U0, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), cons(U0, concat(V'', Z')))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
four new Dependency Pairs are created:
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(V', cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 12
↳Narrowing Transformation
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(V', cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(V', cons(U'', Z''))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(cons(U0, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), cons(U0, concat(V'', Z')))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', V0'')), concat(W, Z))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', V0'), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', V0'), Z')
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U''', V''), V0), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(cons(U''', concat(V'', V0)), cons(U'', Z''))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
two new Dependency Pairs are created:
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', V0'')), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), Z')
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(cons(U0, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), cons(U0, concat(V', Z')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 13
↳Narrowing Transformation
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(cons(U0, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), cons(U0, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), Z')
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(V', cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(cons(U''', V''), V0), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(cons(U''', concat(V'', V0)), cons(U'', Z''))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(V', cons(U'', Z''))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(cons(U0, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), cons(U0, concat(V'', Z')))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), concat(W, Z))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', V0'), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', V0'), Z')
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
four new Dependency Pairs are created:
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(cons(U1, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), cons(U1, concat(V', Z')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 14
↳Narrowing Transformation
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(cons(U1, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), cons(U1, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), Z')
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(V', cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(cons(U''', V''), V0), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(cons(U''', concat(V'', V0)), cons(U'', Z''))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(V', cons(U'', Z''))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(cons(U0, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), cons(U0, concat(V'', Z')))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), Z')
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', V0'), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', V0'), Z')
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(cons(U0, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), cons(U0, concat(V', Z')))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
two new Dependency Pairs are created:
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(V', cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', Z''')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 15
↳Narrowing Transformation
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(V', cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(cons(U0, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), cons(U0, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), Z')
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(V', cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(cons(U''', V''), V0), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(cons(U''', concat(V'', V0)), cons(U'', Z''))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(V', cons(U'', Z''))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(cons(U0, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), cons(U0, concat(V'', Z')))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), Z')
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', V0'), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', V0'), Z')
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(cons(U1, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), cons(U1, concat(V', Z')))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
four new Dependency Pairs are created:
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(V', cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(cons(U'1, V'''), V0), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(cons(U'1, concat(V''', V0)), cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, leaf))), Z'''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, Z''''))))
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, V''')))), Z'''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, cons(U'1, concat(V''', Z''''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 16
↳Narrowing Transformation
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, V''')))), Z'''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, cons(U'1, concat(V''', Z''''))))))
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, leaf))), Z'''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, Z''''))))
LESSLEAVES(cons(cons(U'1, V'''), V0), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(cons(U'1, concat(V''', V0)), cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(V', cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(V', cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(cons(U1, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), cons(U1, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(cons(U0, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), cons(U0, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), Z')
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(V', cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(cons(U''', V''), V0), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(cons(U''', concat(V'', V0)), cons(U'', Z''))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(V', cons(U'', Z''))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(cons(U0, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), cons(U0, concat(V'', Z')))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), Z')
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', V0'), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', V0'), Z')
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', Z''')))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
two new Dependency Pairs are created:
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(cons(U1, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), cons(U1, concat(V', Z')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 17
↳Narrowing Transformation
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(cons(U1, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), cons(U1, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), Z')
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, leaf))), Z'''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, Z''''))))
LESSLEAVES(cons(cons(U'1, V'''), V0), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(cons(U'1, concat(V''', V0)), cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(V', cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(V', cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(cons(U1, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), cons(U1, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(cons(U0, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), cons(U0, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), Z')
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(V', cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(cons(U''', V''), V0), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(cons(U''', concat(V'', V0)), cons(U'', Z''))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(V', cons(U'', Z''))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(cons(U0, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), cons(U0, concat(V'', Z')))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), Z')
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', V0'), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', V0'), Z')
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, V''')))), Z'''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, cons(U'1, concat(V''', Z''''))))))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
four new Dependency Pairs are created:
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, leaf)))), V0''''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, V0'''')))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, cons(U2, V''))))), V0''''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, cons(U2, concat(V'', V0'''')))))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(cons(U2, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), cons(U2, concat(V'', Z')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 18
↳Narrowing Transformation
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(cons(U2, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), cons(U2, concat(V'', Z')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, cons(U2, V''))))), V0''''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, cons(U2, concat(V'', V0'''')))))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, leaf)))), V0''''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, V0'''')))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), Z')
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, V''')))), Z'''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, cons(U'1, concat(V''', Z''''))))))
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, leaf))), Z'''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, Z''''))))
LESSLEAVES(cons(cons(U'1, V'''), V0), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(cons(U'1, concat(V''', V0)), cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(V', cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(V', cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(cons(U1, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), cons(U1, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), Z')
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(cons(U0, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), cons(U0, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), Z')
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(V', cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(cons(U''', V''), V0), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(cons(U''', concat(V'', V0)), cons(U'', Z''))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(V', cons(U'', Z''))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(cons(U0, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), cons(U0, concat(V'', Z')))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), Z')
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', V0'), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', V0'), Z')
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(cons(U1, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), cons(U1, concat(V', Z')))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
two new Dependency Pairs are created:
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, leaf))), Z'''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, Z''''))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', cons(U'0, leaf))), Z'''')) -> LESSLEAVES(V', cons(U'', cons(U''', cons(U'0, Z''''))))
LESSLEAVES(cons(cons(U'1, V''), V0), cons(cons(U'', cons(U''', cons(U'0, leaf))), Z'''')) -> LESSLEAVES(cons(U'1, concat(V'', V0)), cons(U'', cons(U''', cons(U'0, Z''''))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 19
↳Narrowing Transformation
LESSLEAVES(cons(cons(U'1, V''), V0), cons(cons(U'', cons(U''', cons(U'0, leaf))), Z'''')) -> LESSLEAVES(cons(U'1, concat(V'', V0)), cons(U'', cons(U''', cons(U'0, Z''''))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', cons(U'0, leaf))), Z'''')) -> LESSLEAVES(V', cons(U'', cons(U''', cons(U'0, Z''''))))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, cons(U2, V''))))), V0''''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, cons(U2, concat(V'', V0'''')))))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, leaf)))), V0''''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, V0'''')))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(cons(U1, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), cons(U1, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), Z')
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, V''')))), Z'''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, cons(U'1, concat(V''', Z''''))))))
LESSLEAVES(cons(cons(U'1, V'''), V0), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(cons(U'1, concat(V''', V0)), cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(V', cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(V', cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(cons(U1, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), cons(U1, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), Z')
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(cons(U0, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), cons(U0, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), Z')
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(V', cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(cons(U''', V''), V0), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(cons(U''', concat(V'', V0)), cons(U'', Z''))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(V', cons(U'', Z''))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(cons(U0, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), cons(U0, concat(V'', Z')))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), Z')
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', V0'), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', V0'), Z')
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(cons(U2, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), cons(U2, concat(V'', Z')))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))
four new Dependency Pairs are created:
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, V''')))), Z'''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, cons(U'1, concat(V''', Z''''))))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, V''')))), Z'''')) -> LESSLEAVES(V', cons(U'', cons(U''', cons(U'0, cons(U'1, concat(V''', Z''''))))))
LESSLEAVES(cons(cons(U'2, V''), V0), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, V''')))), Z'''')) -> LESSLEAVES(cons(U'2, concat(V'', V0)), cons(U'', cons(U''', cons(U'0, cons(U'1, concat(V''', Z''''))))))
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, leaf)))), Z''''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, cons(U'1, Z''''')))))
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, cons(U'2, V''))))), Z''''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, cons(U'1, cons(U'2, concat(V'', Z''''')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 20
↳Remaining Obligation(s)
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, cons(U'2, V''))))), Z''''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, cons(U'1, cons(U'2, concat(V'', Z''''')))))))
LESSLEAVES(cons(U, V), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, leaf)))), Z''''')) -> LESSLEAVES(concat(U, V), cons(U'', cons(U''', cons(U'0, cons(U'1, Z''''')))))
LESSLEAVES(cons(cons(U'2, V''), V0), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, V''')))), Z'''')) -> LESSLEAVES(cons(U'2, concat(V'', V0)), cons(U'', cons(U''', cons(U'0, cons(U'1, concat(V''', Z''''))))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', cons(U'0, cons(U'1, V''')))), Z'''')) -> LESSLEAVES(V', cons(U'', cons(U''', cons(U'0, cons(U'1, concat(V''', Z''''))))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', cons(U'0, leaf))), Z'''')) -> LESSLEAVES(V', cons(U'', cons(U''', cons(U'0, Z''''))))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(cons(U2, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), cons(U2, concat(V'', Z')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, V')))), V0'''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, concat(V', V0'''))))), Z')
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, cons(U2, V''))))), V0''''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, cons(U2, concat(V'', V0'''')))))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, cons(U1, leaf)))), V0''''), cons(W, Z)) -> LESSLEAVES(cons(U'', cons(U', cons(U0, cons(U1, V0'''')))), concat(W, Z))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(cons(U1, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), cons(U1, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, leaf))), V0'''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, V0'''))), Z')
LESSLEAVES(cons(cons(U'1, V'''), V0), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(cons(U'1, concat(V''', V0)), cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', cons(U'0, V''))), Z''')) -> LESSLEAVES(V', cons(U'', cons(U''', cons(U'0, concat(V'', Z''')))))
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', leaf)), Z''')) -> LESSLEAVES(V', cons(U'', cons(U''', Z''')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(cons(U1, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), cons(U1, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', cons(U0, V''))), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', cons(U0, concat(V'', V0'')))), Z')
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(cons(U0, V'), Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), cons(U0, concat(V', Z')))
LESSLEAVES(cons(cons(U'', cons(U', leaf)), V0''), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', V0'')), Z')
LESSLEAVES(cons(cons(U'0, V''), V0), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(cons(U'0, concat(V'', V0)), cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', cons(U''', V''')), Z'')) -> LESSLEAVES(V', cons(U'', cons(U''', concat(V''', Z''))))
LESSLEAVES(cons(cons(U''', V''), V0), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(cons(U''', concat(V'', V0)), cons(U'', Z''))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', leaf), Z'')) -> LESSLEAVES(V', cons(U'', Z''))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(cons(U0, V''), Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), cons(U0, concat(V'', Z')))
LESSLEAVES(cons(cons(U'', cons(U', V')), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', cons(U', concat(V', V0'))), Z')
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', V0'), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', leaf), V0'), cons(leaf, Z')) -> LESSLEAVES(cons(U'', V0'), Z')
LESSLEAVES(cons(cons(U''', V'''), V0), cons(cons(U'', V''), Z')) -> LESSLEAVES(cons(U''', concat(V''', V0)), cons(U'', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(cons(U'', V''), Z')) -> LESSLEAVES(V', cons(U'', concat(V'', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'', V''), V0), cons(cons(U', V'), Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), cons(U', concat(V', Z')))
LESSLEAVES(cons(cons(U'', V''), V0), cons(leaf, Z')) -> LESSLEAVES(cons(U'', concat(V'', V0)), Z')
LESSLEAVES(cons(leaf, V'), cons(cons(U', V''), Z')) -> LESSLEAVES(V', cons(U', concat(V'', Z')))
LESSLEAVES(cons(leaf, V'), cons(leaf, Z')) -> LESSLEAVES(V', Z')
LESSLEAVES(cons(cons(U'1, V''), V0), cons(cons(U'', cons(U''', cons(U'0, leaf))), Z'''')) -> LESSLEAVES(cons(U'1, concat(V'', V0)), cons(U'', cons(U''', cons(U'0, Z''''))))
concat(leaf, Y) -> Y
concat(cons(U, V), Y) -> cons(U, concat(V, Y))
lessleaves(X, leaf) -> false
lessleaves(leaf, cons(W, Z)) -> true
lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))