Term Rewriting System R:
[X, X1, X2, X3]
aa -> ac
aa -> ad
aa -> a
ab -> ac
ab -> ad
ab -> b
ac -> e
ac -> l
ac -> c
ak -> l
ak -> m
ak -> k
ad -> m
ad -> d
aA -> ah(af(aa), af(ab))
aA -> A
ah(X, X) -> ag(mark(X), mark(X), af(ak))
ah(X1, X2) -> h(X1, X2)
ag(d, X, X) -> aA
ag(X1, X2, X3) -> g(X1, X2, X3)
af(X) -> az(mark(X), X)
af(X) -> f(X)
az(e, X) -> mark(X)
az(X1, X2) -> z(X1, X2)
mark(A) -> aA
mark(a) -> aa
mark(b) -> ab
mark(c) -> ac
mark(d) -> ad
mark(k) -> ak
mark(z(X1, X2)) -> az(mark(X1), X2)
mark(f(X)) -> af(mark(X))
mark(h(X1, X2)) -> ah(mark(X1), mark(X2))
mark(g(X1, X2, X3)) -> ag(mark(X1), mark(X2), mark(X3))
mark(e) -> e
mark(l) -> l
mark(m) -> m

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

AA -> AC
AA -> AD
AB -> AC
AB -> AD
AA' -> AH(af(aa), af(ab))
AA' -> AF(aa)
AA' -> AA
AA' -> AF(ab)
AA' -> AB
AH(X, X) -> AG(mark(X), mark(X), af(ak))
AH(X, X) -> MARK(X)
AH(X, X) -> AF(ak)
AH(X, X) -> AK
AG(d, X, X) -> AA'
AF(X) -> AZ(mark(X), X)
AF(X) -> MARK(X)
AZ(e, X) -> MARK(X)
MARK(A) -> AA'
MARK(a) -> AA
MARK(b) -> AB
MARK(c) -> AC
MARK(d) -> AD
MARK(k) -> AK
MARK(z(X1, X2)) -> AZ(mark(X1), X2)
MARK(z(X1, X2)) -> MARK(X1)
MARK(f(X)) -> AF(mark(X))
MARK(f(X)) -> MARK(X)
MARK(h(X1, X2)) -> AH(mark(X1), mark(X2))
MARK(h(X1, X2)) -> MARK(X1)
MARK(h(X1, X2)) -> MARK(X2)
MARK(g(X1, X2, X3)) -> AG(mark(X1), mark(X2), mark(X3))
MARK(g(X1, X2, X3)) -> MARK(X1)
MARK(g(X1, X2, X3)) -> MARK(X2)
MARK(g(X1, X2, X3)) -> MARK(X3)

Furthermore, R contains one SCC.


   R
DPs
       →DP Problem 1
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

AH(X, X) -> AF(ak)
MARK(g(X1, X2, X3)) -> MARK(X3)
MARK(g(X1, X2, X3)) -> MARK(X2)
MARK(g(X1, X2, X3)) -> MARK(X1)
MARK(g(X1, X2, X3)) -> AG(mark(X1), mark(X2), mark(X3))
MARK(h(X1, X2)) -> MARK(X2)
MARK(h(X1, X2)) -> MARK(X1)
AH(X, X) -> MARK(X)
MARK(h(X1, X2)) -> AH(mark(X1), mark(X2))
MARK(f(X)) -> MARK(X)
MARK(f(X)) -> AF(mark(X))
MARK(z(X1, X2)) -> MARK(X1)
MARK(z(X1, X2)) -> AZ(mark(X1), X2)
AF(X) -> MARK(X)
AA' -> AF(ab)
MARK(A) -> AA'
AZ(e, X) -> MARK(X)
AF(X) -> AZ(mark(X), X)
AA' -> AF(aa)
AG(d, X, X) -> AA'
AH(X, X) -> AG(mark(X), mark(X), af(ak))
AA' -> AH(af(aa), af(ab))


Rules:


aa -> ac
aa -> ad
aa -> a
ab -> ac
ab -> ad
ab -> b
ac -> e
ac -> l
ac -> c
ak -> l
ak -> m
ak -> k
ad -> m
ad -> d
aA -> ah(af(aa), af(ab))
aA -> A
ah(X, X) -> ag(mark(X), mark(X), af(ak))
ah(X1, X2) -> h(X1, X2)
ag(d, X, X) -> aA
ag(X1, X2, X3) -> g(X1, X2, X3)
af(X) -> az(mark(X), X)
af(X) -> f(X)
az(e, X) -> mark(X)
az(X1, X2) -> z(X1, X2)
mark(A) -> aA
mark(a) -> aa
mark(b) -> ab
mark(c) -> ac
mark(d) -> ad
mark(k) -> ak
mark(z(X1, X2)) -> az(mark(X1), X2)
mark(f(X)) -> af(mark(X))
mark(h(X1, X2)) -> ah(mark(X1), mark(X2))
mark(g(X1, X2, X3)) -> ag(mark(X1), mark(X2), mark(X3))
mark(e) -> e
mark(l) -> l
mark(m) -> m


Strategy:

innermost



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