(STRATEGY
    INNERMOST)

(VAR
    x2 x1 x6 x4 x0)
(RULES
    rev#1(Nil()) -> Nil()
    rev#1(Cons(x2,x1)) -> append#2(rev#1(x1),Cons(x2,Nil()))
    append#2(Nil(),Cons(x2,Nil())) -> Cons(x2,Nil())
    append#2(Cons(x6,x4),Cons(x2,Nil())) -> Cons(x6,append#2(x4,Cons(x2,Nil())))
    main(x0) -> rev#1(x0))