YES Problem: :(:(:(:(C(),x),y),z),u) -> :(:(x,z),:(:(:(x,y),z),u)) Proof: DP Processor: DPs: :#(:(:(:(C(),x),y),z),u) -> :#(x,y) :#(:(:(:(C(),x),y),z),u) -> :#(:(x,y),z) :#(:(:(:(C(),x),y),z),u) -> :#(:(:(x,y),z),u) :#(:(:(:(C(),x),y),z),u) -> :#(x,z) :#(:(:(:(C(),x),y),z),u) -> :#(:(x,z),:(:(:(x,y),z),u)) TRS: :(:(:(:(C(),x),y),z),u) -> :(:(x,z),:(:(:(x,y),z),u)) LPO Processor: argument filtering: pi(C) = [] pi(:) = [0,1] pi(:#) = 0 usable rules: :(:(:(:(C(),x),y),z),u) -> :(:(x,z),:(:(:(x,y),z),u)) precedence: :# ~ : ~ C problem: DPs: TRS: :(:(:(:(C(),x),y),z),u) -> :(:(x,z),:(:(:(x,y),z),u)) Qed