1.26/1.36 YES 1.26/1.36 1.26/1.36 Problem: 1.26/1.36 -(+(x(),-(x()))) -> 0() 1.26/1.36 +(x(),-(x())) -> 0() 1.26/1.36 0() -> -(0()) 1.26/1.36 1.26/1.36 Proof: 1.26/1.36 Uncurry Processor: 1.26/1.36 f4(-(),f4(f4(+(),x()),f4(-(),x()))) -> 0() 1.26/1.36 f4(f4(+(),x()),f4(-(),x())) -> 0() 1.26/1.36 0() -> f4(-(),0()) 1.26/1.36 Ground Confluence Processor: 1.26/1.36 NFP by decision procedure. 1.51/1.37 EOF