Term Rewriting System R:
[X, Y, X1, X2, X3]
afact(X) -> aif(azero(mark(X)), s(0), prod(X, fact(p(X))))
afact(X) -> fact(X)
aadd(0, X) -> mark(X)
aadd(s(X), Y) -> s(aadd(mark(X), mark(Y)))
aadd(X1, X2) -> add(X1, X2)
aprod(0, X) -> 0
aprod(s(X), Y) -> aadd(mark(Y), aprod(mark(X), mark(Y)))
aprod(X1, X2) -> prod(X1, X2)
aif(true, X, Y) -> mark(X)
aif(false, X, Y) -> mark(Y)
aif(X1, X2, X3) -> if(X1, X2, X3)
azero(0) -> true
azero(s(X)) -> false
azero(X) -> zero(X)
ap(s(X)) -> mark(X)
ap(X) -> p(X)
mark(fact(X)) -> afact(mark(X))
mark(if(X1, X2, X3)) -> aif(mark(X1), X2, X3)
mark(zero(X)) -> azero(mark(X))
mark(prod(X1, X2)) -> aprod(mark(X1), mark(X2))
mark(p(X)) -> ap(mark(X))
mark(add(X1, X2)) -> aadd(mark(X1), mark(X2))
mark(s(X)) -> s(mark(X))
mark(0) -> 0
mark(true) -> true
mark(false) -> false

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

AFACT(X) -> AIF(azero(mark(X)), s(0), prod(X, fact(p(X))))
AFACT(X) -> AZERO(mark(X))
AFACT(X) -> MARK(X)
AADD(0, X) -> MARK(X)
AADD(s(X), Y) -> AADD(mark(X), mark(Y))
AADD(s(X), Y) -> MARK(X)
AADD(s(X), Y) -> MARK(Y)
APROD(s(X), Y) -> AADD(mark(Y), aprod(mark(X), mark(Y)))
APROD(s(X), Y) -> MARK(Y)
APROD(s(X), Y) -> APROD(mark(X), mark(Y))
APROD(s(X), Y) -> MARK(X)
AIF(true, X, Y) -> MARK(X)
AIF(false, X, Y) -> MARK(Y)
AP(s(X)) -> MARK(X)
MARK(fact(X)) -> AFACT(mark(X))
MARK(fact(X)) -> MARK(X)
MARK(if(X1, X2, X3)) -> AIF(mark(X1), X2, X3)
MARK(if(X1, X2, X3)) -> MARK(X1)
MARK(zero(X)) -> AZERO(mark(X))
MARK(zero(X)) -> MARK(X)
MARK(prod(X1, X2)) -> APROD(mark(X1), mark(X2))
MARK(prod(X1, X2)) -> MARK(X1)
MARK(prod(X1, X2)) -> MARK(X2)
MARK(p(X)) -> AP(mark(X))
MARK(p(X)) -> MARK(X)
MARK(add(X1, X2)) -> AADD(mark(X1), mark(X2))
MARK(add(X1, X2)) -> MARK(X1)
MARK(add(X1, X2)) -> MARK(X2)
MARK(s(X)) -> MARK(X)

Furthermore, R contains one SCC.


   R
DPs
       →DP Problem 1
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

APROD(s(X), Y) -> MARK(X)
APROD(s(X), Y) -> APROD(mark(X), mark(Y))
APROD(s(X), Y) -> MARK(Y)
AADD(s(X), Y) -> MARK(Y)
MARK(s(X)) -> MARK(X)
MARK(add(X1, X2)) -> MARK(X2)
MARK(add(X1, X2)) -> MARK(X1)
AADD(s(X), Y) -> MARK(X)
AADD(s(X), Y) -> AADD(mark(X), mark(Y))
MARK(add(X1, X2)) -> AADD(mark(X1), mark(X2))
MARK(p(X)) -> MARK(X)
AP(s(X)) -> MARK(X)
MARK(p(X)) -> AP(mark(X))
MARK(prod(X1, X2)) -> MARK(X2)
MARK(prod(X1, X2)) -> MARK(X1)
AADD(0, X) -> MARK(X)
APROD(s(X), Y) -> AADD(mark(Y), aprod(mark(X), mark(Y)))
MARK(prod(X1, X2)) -> APROD(mark(X1), mark(X2))
MARK(zero(X)) -> MARK(X)
MARK(if(X1, X2, X3)) -> MARK(X1)
AIF(false, X, Y) -> MARK(Y)
MARK(if(X1, X2, X3)) -> AIF(mark(X1), X2, X3)
MARK(fact(X)) -> MARK(X)
AFACT(X) -> MARK(X)
MARK(fact(X)) -> AFACT(mark(X))
AIF(true, X, Y) -> MARK(X)
AFACT(X) -> AIF(azero(mark(X)), s(0), prod(X, fact(p(X))))


Rules:


afact(X) -> aif(azero(mark(X)), s(0), prod(X, fact(p(X))))
afact(X) -> fact(X)
aadd(0, X) -> mark(X)
aadd(s(X), Y) -> s(aadd(mark(X), mark(Y)))
aadd(X1, X2) -> add(X1, X2)
aprod(0, X) -> 0
aprod(s(X), Y) -> aadd(mark(Y), aprod(mark(X), mark(Y)))
aprod(X1, X2) -> prod(X1, X2)
aif(true, X, Y) -> mark(X)
aif(false, X, Y) -> mark(Y)
aif(X1, X2, X3) -> if(X1, X2, X3)
azero(0) -> true
azero(s(X)) -> false
azero(X) -> zero(X)
ap(s(X)) -> mark(X)
ap(X) -> p(X)
mark(fact(X)) -> afact(mark(X))
mark(if(X1, X2, X3)) -> aif(mark(X1), X2, X3)
mark(zero(X)) -> azero(mark(X))
mark(prod(X1, X2)) -> aprod(mark(X1), mark(X2))
mark(p(X)) -> ap(mark(X))
mark(add(X1, X2)) -> aadd(mark(X1), mark(X2))
mark(s(X)) -> s(mark(X))
mark(0) -> 0
mark(true) -> true
mark(false) -> false


Strategy:

innermost



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