/home/nowonder/forschung/aprove/TPDB05/TRS/AProVE/JFP_Ex17.trs

The program

(VAR x y)
(RULES
nats_active -> add_active(zeros_active) 
hd_active(x) -> hd(x)
zeros_active -> cons(0,zeros) 
tl_active(x) -> tl(x)
incr_active(cons(x,y)) -> cons(s(x),incr(y)) 
mark(nats) -> nats_active 
add_active(cons(x,y)) -> incr_active(cons(x,add(y))) 
mark(zeros) -> zeros_active
hd_active(cons(x,y)) -> mark(x) 
mark(incr(x)) -> incr_active(mark(x)) 
tl_active(cons(x,y)) -> mark(y) 
mark(add(x)) -> add_active(mark(x)) 
nats_active -> nats 
mark(hd(x)) -> hd_active(mark(x)) 
zeros_active -> zeros 
mark(tl(x)) -> tl_active(mark(x)) 
incr_active(x) -> incr(x) 
mark(0) -> 0 
add_active(x) -> add(x) 
mark(s(x)) -> s(x) 
mark(cons(x,y)) -> cons(x,y)
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend