/home/nowonder/forschung/aprove/TPDB05/TRS/LJB01/jones1.trs

The program

(VAR ls a x k)
(RULES
rev(ls) -> r1(ls, empty)
r1(empty, a) -> a
r1(cons(x,k), a) -> r1(k, cons(x,a)))

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend