NO
Rewrite Rules:
   [ len(nil) -> 0,
     len(cons(?x,?xs)) -> s(len(?xs)),
     rev(nil) -> nil,
     rev(cons(?x,?xs)) -> app(rev(?xs),cons(?x,nil)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     len(rev(?xs)) -> len(?xs) ]
Apply Direct Methods...
Inner CPs:
   [ len(nil) = len(nil),
     len(app(rev(?xs_1),cons(?x_1,nil))) = len(cons(?x_1,?xs_1)) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, not WCR
Knuth & Bendix
Direct Methods: not CR

Final result: not CR
new/len-rev.trs: Success(not CR)
(20 msec.)