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