(STRATEGY
    INNERMOST)

(VAR
    x4 x3 x2 x1)
(RULES
    walk#1(Nil()) -> Lam2()
    walk#1(Cons(x4,x3)) -> Lam1(walk#1(x3),Lam3(x4))
    apply#2(Lam1(x3,Lam3(x2)),x1) -> apply#2(x3,Cons(x2,x1))
    apply#2(Lam2(),Cons(x1,x2)) -> Cons(x1,x2)
    main() -> apply#2(walk#1(Cons(S(0())
                                 ,Cons(S(S(0())),Cons(S(S(S(0()))),Nil()))))
                     ,Nil()))