Term Rewriting System R:
[x, y, z]
cons(x, cons(y, z)) -> big
inf(x) -> cons(x, inf(s(x)))
Innermost Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
INF(x) -> CONS(x, inf(s(x)))
INF(x) -> INF(s(x))
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
Dependency Pair:
INF(x) -> INF(s(x))
Rules:
cons(x, cons(y, z)) -> big
inf(x) -> cons(x, inf(s(x)))
Strategy:
innermost
As we are in the innermost case, we can delete all 2 non-usable-rules.
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Non Termination
Dependency Pair:
INF(x) -> INF(s(x))
Rule:
none
Strategy:
innermost
Found an infinite P-chain over R:
P =
INF(x) -> INF(s(x))
R = none
s = INF(x)
evaluates to t =INF(s(x))
Thus, s starts an infinite chain as s matches t.
Innermost Termination of R could not be shown.
Duration:
0:01 minutes