NO Rewrite Rules: [ inc(nil) -> nil, inc(cons(?x,?xs)) -> cons(s(?x),inc(?xs)), app(nil,?ys) -> ?ys, app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)), inc(app(?xs,?ys)) -> app(inc(?xs),inc(?ys)), dec(nil) -> nil, dec(cons(0,?xs)) -> cons(0,dec(?xs)), dec(cons(s(?x),?xs)) -> cons(?x,dec(?xs)), dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)), dec(inc(?xs)) -> ?xs ] Apply Direct Methods... Inner CPs: [ inc(?ys_1) = app(inc(nil),inc(?ys_1)), inc(cons(?x_2,app(?xs_2,?ys_2))) = app(inc(cons(?x_2,?xs_2)),inc(?ys_2)), dec(?ys_1) = app(dec(nil),dec(?ys_1)), dec(cons(?x_2,app(?xs_2,?ys_2))) = app(dec(cons(?x_2,?xs_2)),dec(?ys_2)), dec(nil) = nil, dec(cons(s(?x),inc(?xs))) = cons(?x,?xs), dec(app(inc(?xs_3),inc(?ys_3))) = app(?xs_3,?ys_3) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Final result: not CR new/inc.trs: Success(not CR) (18 msec.)