YES 1: +(x1,0()) -> x1 2: +(x1,s(x2)) -> s(+(x1,x2)) 3: d(0()) -> 0() 4: d(s(x1)) -> s(s(d(x1))) 5: f(0()) -> 0() 6: f(s(x1)) -> +(+(s(x1),s(x1)),s(x1)) 7: f(g(0())) -> +(+(g(0()),g(0())),g(0())) 8: g(x1) -> s(d(x1)) @Rule Labeling --- R 1: +(x1,0()) -> x1 2: +(x1,s(x2)) -> s(+(x1,x2)) 3: d(0()) -> 0() 4: d(s(x1)) -> s(s(d(x1))) 5: f(0()) -> 0() 6: f(s(x1)) -> +(+(s(x1),s(x1)),s(x1)) 7: f(g(0())) -> +(+(g(0()),g(0())),g(0())) 8: g(x1) -> s(d(x1)) --- S 1: +(x1,0()) -> x1 2: +(x1,s(x2)) -> s(+(x1,x2)) 3: d(0()) -> 0() 4: d(s(x1)) -> s(s(d(x1))) 5: f(0()) -> 0() 6: f(s(x1)) -> +(+(s(x1),s(x1)),s(x1)) 7: f(g(0())) -> +(+(g(0()),g(0())),g(0())) 8: g(x1) -> s(d(x1))