- Proof technique for syntax trees.
- Goal: prove P(t) for all trees t in a a language.
- Inductive base: Prove that P holds for all trees in stage1.
- Inductive hypothesis: Assume that P holds for all trees in stages
stagej with j <= i.
- Inductive step: Prove that P holds for all trees in stagei.
- Prove P(t) for all trees t in Expression.
- P(true) holds.
- P(not E) holds assuming that P(E) holds (for arbitrary E).
- P(E1&E2) holds assuming that P(E1) holds and P(E2)
holds (for arbitrary E1, E2).
Syntax rules guide the proof!
Author: Wolfgang Schreiner
Last Modification: March 26, 1998