(from AG01 4.24) (VAR x y) (RULES intlist(nil) -> nil intlist(cons(x,y)) -> cons(s(x),intlist(y)) int(0,0) -> cons(0,nil) int(0,s(y)) -> cons(0,int(s(0),s(y))) int(s(x),0) -> nil int(s(x),s(y)) -> intlist(int(x,y)) ) (STRATEGY INNERMOST)
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend