YES ---- CR(R) ---- R : left-linear, C : CR and CP-closing, and Cdup/R : SN R: b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) CP(R): b(a(a(b(b(a(a(a(a(b(b(___y1))))))))))) -> b(a(a(a(a(b(b(a(a(b(b(___y1))))))))))) b(a(b(b(a(a(a(a(b(b(___y3)))))))))) -> b(b(a(a(b(b(___y3)))))) b(a(b(a(a(a(a(b(a(a(a(a(b(b(___y5)))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(___y5)))))))))))))))))))))))))) b(a(a(b(a(a(a(a(b(a(a(a(a(b(b(___y7))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(___y7))))))))))))))))))) b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(___y9)))))))))))))))) -> b(a(a(b(b(___y9))))) b(a(a(b(b(b(___y11)))))) -> b(a(a(a(a(b(b(a(b(b(___y11)))))))))) b(a(b(b(b(___y13))))) -> b(b(a(b(b(___y13))))) b(a(b(a(a(a(a(b(b(___y15))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(b(___y15))))))))))))))))))))))))) b(a(a(b(a(a(a(a(b(b(___y17)))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(b(___y17)))))))))))))))))) b(a(a(a(b(a(a(a(a(b(b(___y19))))))))))) -> b(a(b(b(___y19)))) b(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(___y21)))))))))))))))))))))))))) -> b(a(a(a(a(b(b(a(b(a(a(a(a(b(___y21)))))))))))))) b(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(___y23))))))))))))))))))))))))) -> b(b(a(b(a(a(a(a(b(___y23))))))))) b(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(___y25))))))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(___y25))))))))))))))))))))))))))))) b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(___y27)))))))))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(___y27)))))))))))))))))))))) b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(___y29))))))))))))))))))))))))))))))) -> b(a(b(a(a(a(a(b(___y29)))))))) b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(___y31))))))))))))))))))) -> b(a(a(a(a(b(b(a(a(b(a(a(a(a(b(___y31))))))))))))))) b(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(___y33)))))))))))))))))) -> b(b(a(a(b(a(a(a(a(b(___y33)))))))))) b(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(___y35)))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(___y35)))))))))))))))))))))))))))))) b(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(___y37))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(___y37))))))))))))))))))))))) b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(___y39)))))))))))))))))))))))) -> b(a(a(b(a(a(a(a(b(___y39))))))))) b(a(a(b(b(___y41))))) -> b(a(a(a(a(b(b(a(a(a(b(a(a(a(a(b(___y41)))))))))))))))) b(a(b(b(___y43)))) -> b(b(a(a(a(b(a(a(a(a(b(___y43))))))))))) b(a(b(a(a(a(a(b(___y45)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(___y45))))))))))))))))))))))))))))))) b(a(a(b(a(a(a(a(b(___y47))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(___y47)))))))))))))))))))))))) b(a(a(a(b(a(a(a(a(b(___y49)))))))))) -> b(a(a(a(b(a(a(a(a(b(___y49)))))))))) critical-pair-closing system C: b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) CR(C): see below. ---- CR(R) ---- R : linear and strongly closed [Huet, 1980] R: b(a(a(b(b(x))))) -> b(a(a(a(a(b(b(x))))))) b(a(b(b(x)))) -> b(b(x)) b(a(b(a(a(a(a(b(x)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(x)))))))))))))))))))))) b(a(a(b(a(a(a(a(b(x))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(x))))))))))))))) b(a(a(a(b(a(a(a(a(b(x)))))))))) -> b(x) CP(R): b(a(a(b(b(a(a(a(a(b(b(___y51))))))))))) -> b(a(a(a(a(b(b(a(a(b(b(___y51))))))))))) b(a(b(b(a(a(a(a(b(b(___y53)))))))))) -> b(b(a(a(b(b(___y53)))))) b(a(b(a(a(a(a(b(a(a(a(a(b(b(___y55)))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(___y55)))))))))))))))))))))))))) b(a(a(b(a(a(a(a(b(a(a(a(a(b(b(___y57))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(b(___y57))))))))))))))))))) b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(b(___y59)))))))))))))))) -> b(a(a(b(b(___y59))))) b(a(a(b(b(b(___y61)))))) -> b(a(a(a(a(b(b(a(b(b(___y61)))))))))) b(a(b(b(b(___y63))))) -> b(b(a(b(b(___y63))))) b(a(b(a(a(a(a(b(b(___y65))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(b(___y65))))))))))))))))))))))))) b(a(a(b(a(a(a(a(b(b(___y67)))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(b(___y67)))))))))))))))))) b(a(a(a(b(a(a(a(a(b(b(___y69))))))))))) -> b(a(b(b(___y69)))) b(a(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(___y71)))))))))))))))))))))))))) -> b(a(a(a(a(b(b(a(b(a(a(a(a(b(___y71)))))))))))))) b(a(b(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(___y73))))))))))))))))))))))))) -> b(b(a(b(a(a(a(a(b(___y73))))))))) b(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(___y75))))))))))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(___y75))))))))))))))))))))))))))))) b(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(___y77)))))))))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(b(a(a(a(a(b(___y77)))))))))))))))))))))) b(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(___y79))))))))))))))))))))))))))))))) -> b(a(b(a(a(a(a(b(___y79)))))))) b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(___y81))))))))))))))))))) -> b(a(a(a(a(b(b(a(a(b(a(a(a(a(b(___y81))))))))))))))) b(a(b(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(___y83)))))))))))))))))) -> b(b(a(a(b(a(a(a(a(b(___y83)))))))))) b(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(___y85)))))))))))))))))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(___y85)))))))))))))))))))))))))))))) b(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(___y87))))))))))))))))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(b(a(a(a(a(b(___y87))))))))))))))))))))))) b(a(a(a(b(a(a(a(a(b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(___y89)))))))))))))))))))))))) -> b(a(a(b(a(a(a(a(b(___y89))))))))) b(a(a(b(b(___y91))))) -> b(a(a(a(a(b(b(a(a(a(b(a(a(a(a(b(___y91)))))))))))))))) b(a(b(b(___y93)))) -> b(b(a(a(a(b(a(a(a(a(b(___y93))))))))))) b(a(b(a(a(a(a(b(___y95)))))))) -> b(a(a(a(a(b(a(a(a(a(b(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(___y95))))))))))))))))))))))))))))))) b(a(a(b(a(a(a(a(b(___y97))))))))) -> b(a(b(a(a(b(a(a(a(b(a(a(a(a(b(a(a(a(b(a(a(a(a(b(___y97)))))))))))))))))))))))) b(a(a(a(b(a(a(a(a(b(___y99)))))))))) -> b(a(a(a(b(a(a(a(a(b(___y99))))))))))