Einsetzen an Position

• t[p : = s] in t an Position p den Term s einsetzen

• Übung: exakte Definition, für Term als Abbildung von Baumbereich

  dazu ist t' : $\mathbb {N}$^* $\hookrightarrow$ Σ zu implementieren

  für t' = t[p : = s] und wenn t, s : $\mathbb {N}$^* $\hookrightarrow$ Σ gegeben

• Übung: ergänzen: t[p₁ : = s₁][p₂ : = s₂] =
  • wenn ..., dann = t[p₂ : = s₂][p₁ : = s₁]
  • sonst = ... (2 Fälle)