Motivation

• wir hatten Äquivalenz-Relation $\approx$ auf Spielen definiert: G $\approx$ H$\iff$ Status von (G - H) ist Null

  das ist semantische Charakterisierung (zweiter gewinnt), erfordert Auswertung (Spielbaum-Bewertung)

• Ziel ist jetzt symbolische Charakterisierung

  durch Umformungsregeln →_U von Spielen (Termen)
  (Weglassen und Ersetzen von Optionen)

• so daß G $\approx$ H$\iff$G→_U^*G' = H'←_U^*H

  semant. Äquivalenz = syntakt. Gleichheit der U-Nf.

• U verwendet doch etwas Semantik (≤ auf Optionen)