Term Rewriting System R:
[X, Y, X1, X2, X3]
af(X) -> aif(mark(X), c, f(true))
af(X) -> f(X)
aif(true, X, Y) -> mark(X)
aif(false, X, Y) -> mark(Y)
aif(X1, X2, X3) -> if(X1, X2, X3)
mark(f(X)) -> af(mark(X))
mark(if(X1, X2, X3)) -> aif(mark(X1), mark(X2), X3)
mark(c) -> c
mark(true) -> true
mark(false) -> false

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

AF(X) -> AIF(mark(X), c, f(true))
AF(X) -> MARK(X)
AIF(true, X, Y) -> MARK(X)
AIF(false, X, Y) -> MARK(Y)
MARK(f(X)) -> AF(mark(X))
MARK(f(X)) -> MARK(X)
MARK(if(X1, X2, X3)) -> AIF(mark(X1), mark(X2), X3)
MARK(if(X1, X2, X3)) -> MARK(X1)
MARK(if(X1, X2, X3)) -> MARK(X2)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

MARK(if(X1, X2, X3)) -> MARK(X2)
MARK(if(X1, X2, X3)) -> MARK(X1)
AIF(false, X, Y) -> MARK(Y)
MARK(if(X1, X2, X3)) -> AIF(mark(X1), mark(X2), X3)
MARK(f(X)) -> MARK(X)
AF(X) -> MARK(X)
MARK(f(X)) -> AF(mark(X))
AIF(true, X, Y) -> MARK(X)
AF(X) -> AIF(mark(X), c, f(true))


Rules:


af(X) -> aif(mark(X), c, f(true))
af(X) -> f(X)
aif(true, X, Y) -> mark(X)
aif(false, X, Y) -> mark(Y)
aif(X1, X2, X3) -> if(X1, X2, X3)
mark(f(X)) -> af(mark(X))
mark(if(X1, X2, X3)) -> aif(mark(X1), mark(X2), X3)
mark(c) -> c
mark(true) -> true
mark(false) -> false


Strategy:

innermost



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