/home/nowonder/forschung/aprove/TPDB05/TRS/nontermin/CSR/Ex14_AEGL02.trs

The program

(VAR X Y)

(RULES 
from(X) -> cons(X,from(s(X)))
length(nil) -> 0
length(cons(X,Y)) -> s(length1(Y))
length1(X) -> length(X)
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend