YES
exiting with thread!
(VAR x y z )
(RULES 
        @(nil,y) -> y
        @(.(x,y),z) -> .(x,@(y,z))
        @(@(x,y),z) -> @(x,@(y,z))
        reviter(nil,y) -> y
        reviter(.(x,y),z) -> reviter(y,.(x,z))
        rev(x) -> reviter(x,nil)
        @(reviter(x,y),z) -> reviter(x,@(y,z))
        
)