YES 1 decompositions #1 ----------- 1: c() -> b() 4: f(f(a())) -> c() @Knuth and Bendix' criterion --- R 1: c() -> b() 4: f(f(a())) -> c() --- S 1: c() -> b() 4: f(f(a())) -> c() NOTE: input TRS is reduced original is 1: c() -> b() 2: a() -> a() 3: b() -> b() 4: f(f(a())) -> c() reduced to 1: c() -> b() 4: f(f(a())) -> c()