YES 1 decompositions #0 ----------- 1: a(s(x)) -> s(a(x)) 2: b(a(b(s(x)))) -> a(b(s(a(x)))) 3: b(a(b(b(x)))) -> a(b(a(b(x)))) 4: a(b(a(a(x)))) -> b(a(b(a(x)))) @Rule Labeling --- R 1: a(s(x)) -> s(a(x)) 2: b(a(b(s(x)))) -> a(b(s(a(x)))) 3: b(a(b(b(x)))) -> a(b(a(b(x)))) 4: a(b(a(a(x)))) -> b(a(b(a(x)))) --- S 1: a(s(x)) -> s(a(x)) 2: b(a(b(s(x)))) -> a(b(s(a(x)))) 3: b(a(b(b(x)))) -> a(b(a(b(x)))) 4: a(b(a(a(x)))) -> b(a(b(a(x))))