17.35/5.36	YES
17.35/5.36	
17.35/5.36	Problem:
17.35/5.36	 +(+(x,y),z) -> +(x,+(y,z))
17.35/5.36	 +(x,y) -> +(y,x)
17.35/5.36	 *(*(x,y),z) -> *(x,*(y,z))
17.35/5.36	 *(x,y) -> *(y,x)
17.35/5.36	 *(+(x,y),z) -> +(*(x,z),*(y,z))
17.35/5.36	 *(x,+(y,z)) -> +(*(x,y),*(x,z))
17.35/5.36	
17.35/5.36	Proof:
17.35/5.36	 Church Rosser Transformation Processor:
17.35/5.36	  strict:
17.35/5.36	   
17.35/5.36	  weak:
17.35/5.36	   
17.35/5.36	  critical peaks: 22
17.35/5.36	   +(+(x163,+(x164,y)),z) <-0|0[]- +(+(+(x163,x164),y),z) -0|[]-> +(+(x163,x164),+(y,z))
17.35/5.36	   +(x166,+(x167,y)) <-0|[]- +(+(x166,x167),y) -1|[]-> +(y,+(x166,x167))
17.35/5.36	   *(+(x169,+(x170,y)),z) <-0|0[]- *(+(+(x169,x170),y),z) -4|[]-> +(*(+(x169,x170),z),*(y,z))
17.35/5.36	   *(x,+(x172,+(x173,z))) <-0|1[]- *(x,+(+(x172,x173),z)) -5|[]-> +(*(x,+(x172,x173)),*(x,z))
17.35/5.36	   +(z,+(x,y)) <-1|[]- +(+(x,y),z) -0|[]-> +(x,+(y,z))
17.35/5.36	   +(+(y,x),z) <-1|0[]- +(+(x,y),z) -0|[]-> +(x,+(y,z))
17.35/5.36	   *(+(y,x),z) <-1|0[]- *(+(x,y),z) -4|[]-> +(*(x,z),*(y,z))
17.35/5.36	   *(x,+(z,y)) <-1|1[]- *(x,+(y,z)) -5|[]-> +(*(x,y),*(x,z))
17.35/5.36	   *(*(x183,*(x184,y)),z) <-2|0[]- *(*(*(x183,x184),y),z) -2|[]-> *(*(x183,x184),*(y,z))
17.35/5.36	   *(x186,*(x187,y)) <-2|[]- *(*(x186,x187),y) -3|[]-> *(y,*(x186,x187))
17.35/5.36	   *(x189,*(x190,+(y,z))) <-2|[]- *(*(x189,x190),+(y,z)) -5|[]-> +(*(*(x189,x190),y),
17.35/5.36	                                                                   *(*(x189,x190),z))
17.35/5.36	   *(z,*(x,y)) <-3|[]- *(*(x,y),z) -2|[]-> *(x,*(y,z))
17.35/5.36	   *(*(y,x),z) <-3|0[]- *(*(x,y),z) -2|[]-> *(x,*(y,z))
17.35/5.36	   *(z,+(x,y)) <-3|[]- *(+(x,y),z) -4|[]-> +(*(x,z),*(y,z))
17.35/5.36	   *(+(y,z),x) <-3|[]- *(x,+(y,z)) -5|[]-> +(*(x,y),*(x,z))
17.35/5.36	   *(+(*(x200,y),*(x201,y)),z) <-4|0[]- *(*(+(x200,x201),y),z) -2|[]-> *(+(x200,x201),*(y,z))
17.35/5.36	   +(*(x203,y),*(x204,y)) <-4|[]- *(+(x203,x204),y) -3|[]-> *(y,+(x203,x204))
17.35/5.36	   +(*(x206,+(y,z)),*(x207,+(y,z))) <-4|[]- *(+(x206,x207),+(y,z)) -5|
17.35/5.36	                                            []-> +(*(+(x206,x207),y),*(+(x206,x207),z))
17.35/5.36	   +(*(*(x,y),x210),*(*(x,y),x211)) <-5|[]- *(*(x,y),+(x210,x211)) -2|[]-> *(x,*(y,+(x210,x211)))
17.35/5.36	   *(+(*(x,x213),*(x,x214)),z) <-5|0[]- *(*(x,+(x213,x214)),z) -2|[]-> *(x,*(+(x213,x214),z))
17.35/5.36	   +(*(x,x216),*(x,x217)) <-5|[]- *(x,+(x216,x217)) -3|[]-> *(+(x216,x217),x)
17.35/5.36	   +(*(+(x,y),x219),*(+(x,y),x220)) <-5|[]- *(+(x,y),+(x219,x220)) -4|
17.35/5.36	                                            []-> +(*(x,+(x219,x220)),*(y,+(x219,x220)))
17.35/5.36	  Redundant Rules Transformation:
17.35/5.36	   +(+(x,y),z) -> +(x,+(y,z))
17.35/5.36	   +(x,y) -> +(y,x)
17.35/5.36	   *(*(x,y),z) -> *(x,*(y,z))
17.35/5.36	   *(x,y) -> *(y,x)
17.35/5.36	   *(x,+(y,z)) -> +(*(x,y),*(x,z))
17.35/5.36	   Church Rosser Transformation Processor (ac):
17.35/5.36	    f3_AC(x,f2_AC(y,z)) -> f2_AC(f3_AC(x,y),f3_AC(x,z))
17.35/5.36	    AC critical peaks: joinable
17.35/5.36	    AC-RPO Processor:
17.35/5.36	     precedence:
17.35/5.36	      f3_AC > f2_AC
17.35/5.36	     status:
17.35/5.36	      
17.35/5.36	     problem:
17.35/5.36	      
17.35/5.36	     Qed
17.35/5.37	EOF