NO Termination Proof using AProVETerm Rewriting System R:
[N, V, V1]
U11(tt, N) -> U12(is'Inf(s-osb-Nat-csb(s-osb-Nat-csb(N))))
U12(tt) -> tt
U21(tt) -> tt
U31(tt) -> tt
is'Inf(V) -> isInf(V)
is'Nat(V) -> isNat(V)
is'Thruth(V) -> isThruth(V)
isInf(s-osb-Nat-csb(N)) -> U11(isNat(N), N)
isNat(0) -> tt
isNat(V) -> U21(is'Inf(V))
isNat(s-osb-Nat-csb(V1)) -> U31(isNat(V1))
isThruth(tt) -> tt

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

U11'(tt, N) -> U12'(is'Inf(s-osb-Nat-csb(s-osb-Nat-csb(N))))
U11'(tt, N) -> IS'INF(s-osb-Nat-csb(s-osb-Nat-csb(N)))
IS'INF(V) -> ISINF(V)
IS'THRUTH(V) -> ISTHRUTH(V)
ISNAT(V) -> U21'(is'Inf(V))
ISNAT(V) -> IS'INF(V)
ISNAT(s-osb-Nat-csb(V1)) -> U31'(isNat(V1))
ISNAT(s-osb-Nat-csb(V1)) -> ISNAT(V1)
IS'NAT(V) -> ISNAT(V)
ISINF(s-osb-Nat-csb(N)) -> U11'(isNat(N), N)
ISINF(s-osb-Nat-csb(N)) -> ISNAT(N)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Non Termination


Dependency Pairs:

ISNAT(s-osb-Nat-csb(V1)) -> ISNAT(V1)
ISNAT(V) -> IS'INF(V)
ISINF(s-osb-Nat-csb(N)) -> ISNAT(N)
ISINF(s-osb-Nat-csb(N)) -> U11'(isNat(N), N)
IS'INF(V) -> ISINF(V)
U11'(tt, N) -> IS'INF(s-osb-Nat-csb(s-osb-Nat-csb(N)))


Rules:


U11(tt, N) -> U12(is'Inf(s-osb-Nat-csb(s-osb-Nat-csb(N))))
U12(tt) -> tt
is'Inf(V) -> isInf(V)
is'Thruth(V) -> isThruth(V)
isThruth(tt) -> tt
U31(tt) -> tt
isNat(V) -> U21(is'Inf(V))
isNat(s-osb-Nat-csb(V1)) -> U31(isNat(V1))
isNat(0) -> tt
U21(tt) -> tt
is'Nat(V) -> isNat(V)
isInf(s-osb-Nat-csb(N)) -> U11(isNat(N), N)





Found an infinite P-chain over R:
P =

ISNAT(s-osb-Nat-csb(V1)) -> ISNAT(V1)
ISNAT(V) -> IS'INF(V)
ISINF(s-osb-Nat-csb(N)) -> ISNAT(N)
ISINF(s-osb-Nat-csb(N)) -> U11'(isNat(N), N)
IS'INF(V) -> ISINF(V)
U11'(tt, N) -> IS'INF(s-osb-Nat-csb(s-osb-Nat-csb(N)))

R =

U11(tt, N) -> U12(is'Inf(s-osb-Nat-csb(s-osb-Nat-csb(N))))
U12(tt) -> tt
is'Inf(V) -> isInf(V)
is'Thruth(V) -> isThruth(V)
isThruth(tt) -> tt
U31(tt) -> tt
isNat(V) -> U21(is'Inf(V))
isNat(s-osb-Nat-csb(V1)) -> U31(isNat(V1))
isNat(0) -> tt
U21(tt) -> tt
is'Nat(V) -> isNat(V)
isInf(s-osb-Nat-csb(N)) -> U11(isNat(N), N)

s = IS'INF(s-osb-Nat-csb(0))
evaluates to t =IS'INF(s-osb-Nat-csb(0))

Thus, s starts an infinite chain.

Non-Termination of R could be shown.
Duration:
0:03 minutes