YES (ignored inputs)COMMENT the following rules are removed from the original TRS + ( x , 0 ( ) ) -> x + ( x , s ( y ) ) -> s ( + ( x , y ) ) d ( 0 ( ) ) -> 0 ( ) d ( s ( x ) ) -> s ( s ( d ( x ) ) ) f ( 0 ( ) ) -> 0 ( ) f ( s ( x ) ) -> + ( + ( s ( x ) , s ( x ) ) , s ( x ) ) f ( g ( 0 ( ) ) ) -> + ( + ( g ( 0 ( ) ) , g ( 0 ( ) ) ) , g ( 0 ( ) ) ) g ( x ) -> s ( d ( x ) ) : CR Combined result: CR /tmp/fileTjODl2.trs: Success(CR) (0 msec.)