Beispiel(4) Schritt 3: Entfernen nicht mehr erreichbarer Knoten Neu entstandener Termgraph: s(0) +((s(0) x (0 + y)) + (s(0) x (0 + y) Formen der Termgraphersetzung Reine Termgraphersetzung Termgraphersetzung mit Zusammenfalten Termgraphersetzung mit Auswalzen Es gibt auch eine Variante mit beiden Operationen. Vollständigkeit Termgraphersetzung mit Zusammenfalten und mit Auswalzen unvollständig für: Berechnen von Normalformen Simulieren von Termersetzungen Vollständig: Überprüfen der Gültigkeit von Gleichungen Berechnen von Term Normalformen mit Hilfe einer Subklasse der Termersetzungsysteme Terminierung Termgraphersetzung terminiert, wenn entsprechende Termersetzung terminiert Beispiel:  (1) f(a,b,x) -> f(x,x,x) (2) a -> b Ableitung: f(a,b,a) ->f(a,a,a) ->f(a,b,a)->.... Termersetzung terminiert nicht. Aber Termgraphersetzung (mit Zusammenfalten) terminiert!