Term-Gleichungen

funktionales Programm = Gleichungssystem

• Grundbereich ist Menge der Terme (Bäume)
• Gleichungen sind die Funktionsdefinitionen

Beweis von Programm-Eigenschaften durch

• equational reasoning

  (äquivalentes Umformen, Ersetzen von Teiltermen durch gleichwertige)

• Induktion (nach dem Termaufbau)