(VAR f m n x xs y )
(RULES 
        app'(app'(eq,0),0) -> true
        app'(app'(eq,0),app'(s,x)) -> false
        app'(app'(eq,app'(s,x)),0) -> false
        app'(app'(eq,app'(s,x)),app'(s,y)) -> app'(app'(eq,x),y)
        app'(app'(le,0),y) -> true
        app'(app'(le,app'(s,x)),0) -> false
        app'(app'(le,app'(s,x)),app'(s,y)) -> app'(app'(le,x),y)
        app'(app'(app,nil),y) -> y
        app'(app'(app,app'(app'(add,n),x)),y) -> app'(app'(add,n),app'(app'(app,x),y))
        app'(min,app'(app'(add,n),nil)) -> n
        app'(min,app'(app'(add,n),app'(app'(add,m),x))) -> app'(app'(if_min,app'(app'(le,n),m)),app'(app'(add,n),app'(app'(add,m),x)))
        app'(app'(if_min,true),app'(app'(add,n),app'(app'(add,m),x))) -> app'(min,app'(app'(add,n),x))
        app'(app'(if_min,false),app'(app'(add,n),app'(app'(add,m),x))) -> app'(min,app'(app'(add,m),x))
        app'(app'(rm,n),nil) -> nil
        app'(app'(rm,n),app'(app'(add,m),x)) -> app'(app'(app'(if_rm,app'(app'(eq,n),m)),n),app'(app'(add,m),x))
        app'(app'(app'(if_rm,true),n),app'(app'(add,m),x)) -> app'(app'(rm,n),x)
        app'(app'(app'(if_rm,false),n),app'(app'(add,m),x)) -> app'(app'(add,m),app'(app'(rm,n),x))
        app'(app'(minsort,nil),nil) -> nil
        app'(app'(minsort,app'(app'(add,n),x)),y) -> app'(app'(app'(if_minsort,app'(app'(eq,n),app'(min,app'(app'(add,n),x)))),app'(app'(add,n),x)),y)
        app'(app'(app'(if_minsort,true),app'(app'(add,n),x)),y) -> app'(app'(add,n),app'(app'(minsort,app'(app'(app,app'(app'(rm,n),x)),y)),nil))
        app'(app'(app'(if_minsort,false),app'(app'(add,n),x)),y) -> app'(app'(minsort,x),app'(app'(add,n),y))
        app'(app'(map,f),nil) -> nil
        app'(app'(map,f),app'(app'(add,x),xs)) -> app'(app'(add,app'(f,x)),app'(app'(map,f),xs))
        app'(app'(filter,f),nil) -> nil
        app'(app'(filter,f),app'(app'(add,x),xs)) -> app'(app'(app'(app'(filter2,app'(f,x)),f),x),xs)
        app'(app'(app'(app'(filter2,true),f),x),xs) -> app'(app'(add,x),app'(app'(filter,f),xs))
        app'(app'(app'(app'(filter2,false),f),x),xs) -> app'(app'(filter,f),xs)
        
)