Church-Rosser property and unique normal form property of nonduplicting term rewriting systems

The original idea of the conditional linearization of non-left-linear term rewriting systems was introduced by De Vrijer [4], Klop and De Vrijer [7] for giving a simpler proof of Chew’s theorem $[2, 10] $. They developed an interesting method for proving the unique normal form property for some non-Church-Rosser, non-left-linear term rewriting system $R $. The method is based on th