/home/nowonder/forschung/aprove/TPDB05/TRS/AProVE/Liveness6.2.trs

The program

(VAR x y)
(RULES
top(sent(x)) -> top(check(rest(x)))
rest(nil) -> sent(nil)
rest(cons(x,y)) -> sent(y)
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
check(cons(x,y)) -> cons(x,y)
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend