habe aus Regeln 1 und 1 die folgenden kritischen Paare erzeugt 1. krit Paar: f(f(x,y),f(z,Z)) = f(f(x,f(y,z)),Z) habe Gleichung f(f(x,y),f(z,Z)) = f(f(x,f(y,z)),Z) zu f(x,f(y,f(z,Z))) = f(f(x,f(y,z)),Z) reduziert. habe Gleichung f(x,f(y,f(z,Z))) = f(f(x,f(y,z)),Z) zu f(x,f(y,f(z,Z))) = f(x,f(f(y,z),Z)) reduziert. habe Gleichung f(x,f(y,f(z,Z))) = f(x,f(f(y,z),Z)) zu f(x,f(y,f(z,Z))) = f(x,f(y,f(z,Z))) reduziert. habe trivial-Gleichung f(x,f(y,f(z,Z))) = f(x,f(y,f(z,Z))) geloescht habe aus Regeln 1 und 2 die folgenden kritischen Paare erzeugt 2. krit Paar: f(e,f(X,z)) = f(X,z) habe Gleichung f(e,f(X,z)) = f(X,z) zu f(X,z) = f(X,z) reduziert. habe trivial-Gleichung f(X,z) = f(X,z) geloescht habe aus Regeln 2 und 3 die folgenden kritischen Paare erzeugt 3. krit Paar: ie = e habe Gleichung ie = e orientiert. 5: ie -> e habe aus Regeln 3 und 1 die folgenden kritischen Paare erzeugt 4. krit Paar: f(x,f(ix,X)) = f(e,X) 5. krit Paar: e = f(y,f(z,if(y,z))) habe Gleichung f(x,f(ix,X)) = f(e,X) zu f(x,f(ix,X)) = X reduziert. habe Gleichung e = f(y,f(z,if(y,z))) zu e = f(y,f(z,f(iz,iy))) reduziert. habe Gleichung f(x,f(ix,X)) = X orientiert. 6: f(x,f(ix,y)) -> y habe Gleichung e = f(y,f(z,f(iz,iy))) zu e = f(y,iy) reduziert. habe Gleichung e = f(y,iy) zu e = e reduziert. habe trivial-Gleichung e = e geloescht habe aus Regeln 1 und 6 die folgenden kritischen Paare erzeugt 6. krit Paar: f(x,f(y,f(if(x,y),Y))) = Y 7. krit Paar: f(X,f(f(iX,Y),z)) = f(Y,z) habe Gleichung f(x,f(y,f(if(x,y),Y))) = Y zu f(x,f(y,f(f(iy,ix),Y))) = Y reduziert. habe Gleichung f(x,f(y,f(f(iy,ix),Y))) = Y zu f(x,f(y,f(iy,f(ix,Y)))) = Y reduziert. habe Gleichung f(x,f(y,f(iy,f(ix,Y)))) = Y zu f(x,f(ix,Y)) = Y reduziert. habe Gleichung f(x,f(ix,Y)) = Y zu Y = Y reduziert. habe Gleichung f(X,f(f(iX,Y),z)) = f(Y,z) zu f(X,f(iX,f(Y,z))) = f(Y,z) reduziert. habe Gleichung f(X,f(iX,f(Y,z))) = f(Y,z) zu f(Y,z) = f(Y,z) reduziert. habe trivial-Gleichung Y = Y geloescht habe trivial-Gleichung f(Y,z) = f(Y,z) geloescht habe aus Regeln 3 und 6 die folgenden kritischen Paare erzeugt 8. krit Paar: iiy = f(y,e) habe Gleichung iiy = f(y,e) orientiert. 7: iix -> f(x,e) habe aus Regeln 2 und 6 die folgenden kritischen Paare erzeugt 9. krit Paar: f(ie,z) = z habe Gleichung f(ie,z) = z zu f(e,z) = z reduziert. habe Gleichung f(e,z) = z zu z = z reduziert. habe trivial-Gleichung z = z geloescht habe aus Regeln 6 und 6 die folgenden kritischen Paare erzeugt 10. krit Paar: f(iiz,y) = f(z,y) habe Gleichung f(iiz,y) = f(z,y) zu f(f(z,e),y) = f(z,y) reduziert. habe Gleichung f(f(z,e),y) = f(z,y) zu f(z,f(e,y)) = f(z,y) reduziert. habe Gleichung f(z,f(e,y)) = f(z,y) zu f(z,y) = f(z,y) reduziert. habe trivial-Gleichung f(z,y) = f(z,y) geloescht habe aus Regeln 6 und 7 die folgenden kritischen Paare erzeugt 11. krit Paar: y = f(iz,f(f(z,e),y)) habe Gleichung y = f(iz,f(f(z,e),y)) zu y = f(iz,f(z,f(e,y))) reduziert. habe Gleichung y = f(iz,f(z,f(e,y))) zu y = f(iz,f(z,y)) reduziert. habe Gleichung y = f(iz,f(z,y)) orientiert. 8: f(ix,f(x,y)) -> y habe aus Regeln 3 und 7 die folgenden kritischen Paare erzeugt 12. krit Paar: e = f(iy,f(y,e)) habe Gleichung e = f(iy,f(y,e)) zu e = e reduziert. habe trivial-Gleichung e = e geloescht habe aus Regeln 7 und 7 die folgenden kritischen Paare erzeugt 13. krit Paar: f(ix,e) = if(x,e) habe Gleichung f(ix,e) = if(x,e) zu f(ix,e) = f(ie,ix) reduziert. habe Gleichung f(ix,e) = f(ie,ix) zu f(ix,e) = f(e,ix) reduziert. habe Gleichung f(ix,e) = f(e,ix) zu f(ix,e) = ix reduziert. habe Gleichung f(ix,e) = ix orientiert. 9: f(ix,e) -> ix habe aus Regeln 7 und 9 die folgenden kritischen Paare erzeugt 14. krit Paar: iix = f(f(x,e),e) habe Gleichung iix = f(f(x,e),e) zu f(x,e) = f(f(x,e),e) reduziert. habe Gleichung f(x,e) = f(f(x,e),e) zu f(x,e) = f(x,f(e,e)) reduziert. habe Gleichung f(x,e) = f(x,f(e,e)) zu f(x,e) = f(x,e) reduziert. habe trivial-Gleichung f(x,e) = f(x,e) geloescht habe aus Regeln 6 und 9 die folgenden kritischen Paare erzeugt 15. krit Paar: e = f(z,iz) habe Gleichung e = f(z,iz) zu e = e reduziert. habe trivial-Gleichung e = e geloescht habe aus Regeln 1 und 9 die folgenden kritischen Paare erzeugt 16. krit Paar: f(iX,f(e,z)) = f(iX,z) habe Gleichung f(iX,f(e,z)) = f(iX,z) zu f(iX,z) = f(iX,z) reduziert. habe trivial-Gleichung f(iX,z) = f(iX,z) geloescht habe aus Regeln 1 und 4 die folgenden kritischen Paare erzeugt 17. krit Paar: f(iz,if(x,y)) = if(x,f(y,z)) habe Gleichung f(iz,if(x,y)) = if(x,f(y,z)) zu f(iz,f(iy,ix)) = if(x,f(y,z)) reduziert. habe Gleichung f(iz,f(iy,ix)) = if(x,f(y,z)) zu f(iz,f(iy,ix)) = f(if(y,z),ix) reduziert. habe Gleichung f(iz,f(iy,ix)) = f(if(y,z),ix) zu f(iz,f(iy,ix)) = f(f(iz,iy),ix) reduziert. habe Gleichung f(iz,f(iy,ix)) = f(f(iz,iy),ix) zu f(iz,f(iy,ix)) = f(iz,f(iy,ix)) reduziert. habe trivial-Gleichung f(iz,f(iy,ix)) = f(iz,f(iy,ix)) geloescht habe aus Regeln 2 und 4 die folgenden kritischen Paare erzeugt 18. krit Paar: f(ix,ie) = ix habe Gleichung f(ix,ie) = ix zu f(ix,e) = ix reduziert. habe Gleichung f(ix,e) = ix zu ix = ix reduziert. habe trivial-Gleichung ix = ix geloescht habe aus Regeln 3 und 4 die folgenden kritischen Paare erzeugt 19. krit Paar: f(iix,ix) = ie 20. krit Paar: e = f(f(y,z),f(iz,iy)) habe Gleichung f(iix,ix) = ie zu f(f(x,e),ix) = ie reduziert. habe Gleichung f(f(x,e),ix) = ie zu f(x,f(e,ix)) = ie reduziert. habe Gleichung f(x,f(e,ix)) = ie zu f(x,ix) = ie reduziert. habe Gleichung f(x,ix) = ie zu e = ie reduziert. habe Gleichung e = ie zu e = e reduziert. habe Gleichung e = f(f(y,z),f(iz,iy)) zu e = f(y,f(z,f(iz,iy))) reduziert. habe Gleichung e = f(y,f(z,f(iz,iy))) zu e = f(y,iy) reduziert. habe Gleichung e = f(y,iy) zu e = e reduziert. habe trivial-Gleichung e = e geloescht habe trivial-Gleichung e = e geloescht habe aus Regeln 3 und 5 die folgenden kritischen Paare erzeugt 21. krit Paar: e = f(e,e) habe Gleichung e = f(e,e) zu e = e reduziert. habe trivial-Gleichung e = e geloescht habe aus Regeln 5 und 6 die folgenden kritischen Paare erzeugt 22. krit Paar: y = f(e,f(e,y)) habe Gleichung y = f(e,f(e,y)) zu y = f(e,y) reduziert. habe Gleichung y = f(e,y) zu y = y reduziert. habe trivial-Gleichung y = y geloescht habe aus Regeln 4 und 6 die folgenden kritischen Paare erzeugt 23. krit Paar: X = f(f(x,y),f(f(iy,ix),X)) 24. krit Paar: f(if(iz,X),iz) = iX habe Gleichung X = f(f(x,y),f(f(iy,ix),X)) zu X = f(x,f(y,f(f(iy,ix),X))) reduziert. habe Gleichung X = f(x,f(y,f(f(iy,ix),X))) zu X = f(x,f(y,f(iy,f(ix,X)))) reduziert. habe Gleichung X = f(x,f(y,f(iy,f(ix,X)))) zu X = f(x,f(ix,X)) reduziert. habe Gleichung X = f(x,f(ix,X)) zu X = X reduziert. habe Gleichung f(if(iz,X),iz) = iX zu f(f(iX,iiz),iz) = iX reduziert. habe Gleichung f(f(iX,iiz),iz) = iX zu f(iX,f(iiz,iz)) = iX reduziert. habe Gleichung f(iX,f(iiz,iz)) = iX zu f(iX,f(f(z,e),iz)) = iX reduziert. habe Gleichung f(iX,f(f(z,e),iz)) = iX zu f(iX,f(z,f(e,iz))) = iX reduziert. habe Gleichung f(iX,f(z,f(e,iz))) = iX zu f(iX,f(z,iz)) = iX reduziert. habe Gleichung f(iX,f(z,iz)) = iX zu f(iX,e) = iX reduziert. habe Gleichung f(iX,e) = iX zu iX = iX reduziert. habe trivial-Gleichung X = X geloescht habe trivial-Gleichung iX = iX geloescht habe aus Regeln 5 und 7 die folgenden kritischen Paare erzeugt 25. krit Paar: f(e,e) = ie habe Gleichung f(e,e) = ie zu e = ie reduziert. habe Gleichung e = ie zu e = e reduziert. habe trivial-Gleichung e = e geloescht habe aus Regeln 4 und 7 die folgenden kritischen Paare erzeugt 26. krit Paar: f(f(x,y),e) = if(iy,ix) habe Gleichung f(f(x,y),e) = if(iy,ix) zu f(x,f(y,e)) = if(iy,ix) reduziert. habe Gleichung f(x,f(y,e)) = if(iy,ix) zu f(x,f(y,e)) = f(iix,iiy) reduziert. habe Gleichung f(x,f(y,e)) = f(iix,iiy) zu f(x,f(y,e)) = f(f(x,e),iiy) reduziert. habe Gleichung f(x,f(y,e)) = f(f(x,e),iiy) zu f(x,f(y,e)) = f(x,f(e,iiy)) reduziert. habe Gleichung f(x,f(y,e)) = f(x,f(e,iiy)) zu f(x,f(y,e)) = f(x,iiy) reduziert. habe Gleichung f(x,f(y,e)) = f(x,iiy) zu f(x,f(y,e)) = f(x,f(y,e)) reduziert. habe trivial-Gleichung f(x,f(y,e)) = f(x,f(y,e)) geloescht habe aus Regeln 7 und 8 die folgenden kritischen Paare erzeugt 27. krit Paar: z = f(f(x,e),f(ix,z)) habe Gleichung z = f(f(x,e),f(ix,z)) zu z = f(x,f(e,f(ix,z))) reduziert. habe Gleichung z = f(x,f(e,f(ix,z))) zu z = f(x,f(ix,z)) reduziert. habe Gleichung z = f(x,f(ix,z)) zu z = z reduziert. habe trivial-Gleichung z = z geloescht habe aus Regeln 6 und 8 die folgenden kritischen Paare erzeugt 28. krit Paar: f(ix,y) = f(ix,y) 29. krit Paar: f(z,X) = f(z,X) habe trivial-Gleichung f(ix,y) = f(ix,y) geloescht habe trivial-Gleichung f(z,X) = f(z,X) geloescht habe aus Regeln 5 und 8 die folgenden kritischen Paare erzeugt 30. krit Paar: y = f(e,f(e,y)) habe Gleichung y = f(e,f(e,y)) zu y = f(e,y) reduziert. habe Gleichung y = f(e,y) zu y = y reduziert. habe trivial-Gleichung y = y geloescht habe aus Regeln 4 und 8 die folgenden kritischen Paare erzeugt 31. krit Paar: X = f(f(iy,ix),f(f(x,y),X)) 32. krit Paar: f(if(z,X),iiz) = iX habe Gleichung X = f(f(iy,ix),f(f(x,y),X)) zu X = f(iy,f(ix,f(f(x,y),X))) reduziert. habe Gleichung X = f(iy,f(ix,f(f(x,y),X))) zu X = f(iy,f(ix,f(x,f(y,X)))) reduziert. habe Gleichung X = f(iy,f(ix,f(x,f(y,X)))) zu X = f(iy,f(y,X)) reduziert. habe Gleichung X = f(iy,f(y,X)) zu X = X reduziert. habe Gleichung f(if(z,X),iiz) = iX zu f(f(iX,iz),iiz) = iX reduziert. habe Gleichung f(f(iX,iz),iiz) = iX zu f(iX,f(iz,iiz)) = iX reduziert. habe Gleichung f(iX,f(iz,iiz)) = iX zu f(iX,e) = iX reduziert. habe Gleichung f(iX,e) = iX zu iX = iX reduziert. habe trivial-Gleichung X = X geloescht habe trivial-Gleichung iX = iX geloescht habe aus Regeln 1 und 8 die folgenden kritischen Paare erzeugt 33. krit Paar: z = f(if(x,y),f(x,f(y,z))) 34. krit Paar: f(iX,f(f(X,Y),z)) = f(Y,z) habe Gleichung z = f(if(x,y),f(x,f(y,z))) zu z = f(f(iy,ix),f(x,f(y,z))) reduziert. habe Gleichung z = f(f(iy,ix),f(x,f(y,z))) zu z = f(iy,f(ix,f(x,f(y,z)))) reduziert. habe Gleichung z = f(iy,f(ix,f(x,f(y,z)))) zu z = f(iy,f(y,z)) reduziert. habe Gleichung z = f(iy,f(y,z)) zu z = z reduziert. habe Gleichung f(iX,f(f(X,Y),z)) = f(Y,z) zu f(iX,f(X,f(Y,z))) = f(Y,z) reduziert. habe Gleichung f(iX,f(X,f(Y,z))) = f(Y,z) zu f(Y,z) = f(Y,z) reduziert. habe trivial-Gleichung z = z geloescht habe trivial-Gleichung f(Y,z) = f(Y,z) geloescht habe aus Regeln 3 und 8 die folgenden kritischen Paare erzeugt 35. krit Paar: ix = f(ix,e) habe Gleichung ix = f(ix,e) zu ix = ix reduziert. habe trivial-Gleichung ix = ix geloescht habe aus Regeln 2 und 8 die folgenden kritischen Paare erzeugt 36. krit Paar: x = f(ie,x) habe Gleichung x = f(ie,x) zu x = f(e,x) reduziert. habe Gleichung x = f(e,x) zu x = x reduziert. habe trivial-Gleichung x = x geloescht habe aus Regeln 8 und 8 die folgenden kritischen Paare erzeugt 37. krit Paar: f(x,y) = f(iix,y) habe Gleichung f(x,y) = f(iix,y) zu f(x,y) = f(f(x,e),y) reduziert. habe Gleichung f(x,y) = f(f(x,e),y) zu f(x,y) = f(x,f(e,y)) reduziert. habe Gleichung f(x,y) = f(x,f(e,y)) zu f(x,y) = f(x,y) reduziert. habe trivial-Gleichung f(x,y) = f(x,y) geloescht habe aus Regeln 8 und 9 die folgenden kritischen Paare erzeugt 38. krit Paar: e = f(iiz,iz) habe Gleichung e = f(iiz,iz) zu e = f(f(z,e),iz) reduziert. habe Gleichung e = f(f(z,e),iz) zu e = f(z,f(e,iz)) reduziert. habe Gleichung e = f(z,f(e,iz)) zu e = f(z,iz) reduziert. habe Gleichung e = f(z,iz) zu e = e reduziert. habe trivial-Gleichung e = e geloescht habe aus Regeln 5 und 9 die folgenden kritischen Paare erzeugt 39. krit Paar: ie = f(e,e) habe Gleichung ie = f(e,e) zu e = f(e,e) reduziert. habe Gleichung e = f(e,e) zu e = e reduziert. habe trivial-Gleichung e = e geloescht habe aus Regeln 4 und 9 die folgenden kritischen Paare erzeugt 40. krit Paar: if(x,y) = f(f(iy,ix),e) 41. krit Paar: f(ie,iiz) = iiz habe Gleichung if(x,y) = f(f(iy,ix),e) zu f(iy,ix) = f(f(iy,ix),e) reduziert. habe Gleichung f(iy,ix) = f(f(iy,ix),e) zu f(iy,ix) = f(iy,f(ix,e)) reduziert. habe Gleichung f(iy,ix) = f(iy,f(ix,e)) zu f(iy,ix) = f(iy,ix) reduziert. habe Gleichung f(ie,iiz) = iiz zu f(e,iiz) = iiz reduziert. habe Gleichung f(e,iiz) = iiz zu iiz = iiz reduziert. habe Gleichung iiz = iiz zu f(z,e) = iiz reduziert. habe Gleichung f(z,e) = iiz zu f(z,e) = f(z,e) reduziert. habe trivial-Gleichung f(iy,ix) = f(iy,ix) geloescht habe trivial-Gleichung f(z,e) = f(z,e) geloescht Final result: 2: f(e,x) -> x 3: f(x,ix) -> e 1: f(f(x,y),z) -> f(x,f(y,z)) 4: if(x,y) -> f(iy,ix) 5: ie -> e 6: f(x,f(ix,y)) -> y 7: iix -> f(x,e) 8: f(ix,f(x,y)) -> y 9: f(ix,e) -> ix