Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex8_BLR02_L)

The rewrite relation of the following TRS is considered.

sel(s(N),cons(X)) → sel(N,XS) (1)
fib(N) → sel(N,fib1(s(0),s(0))) (2)
fib1(X,Y) → cons(X) (3)
add(0,X) → X (4)
add(s(X),Y) → s(add(X,Y)) (5)
sel(0,cons(X)) → X (6)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Variable Condition Violated

The TRS violates one of the two variable conditions. Thus, it is not terminating.