Go backward to Induction and RecursionGo up to TopGo forward to Unicity of Typing |

- 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`stage`._{1} - Inductive hypothesis: Assume that
*P*holds for all trees in stages`stage`with_{j}*j <= i*. - Inductive step: Prove that
*P*holds for all trees in`stage`._{i}

- Goal: prove
- 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*(E&E_{1}) holds assuming that_{2}*P*(E) holds and_{1}*P*(E) holds (for arbitrary E_{2}, E_{1})._{2}

*Syntax rules guide the proof!*

Author: Wolfgang Schreiner

Last Modification: March 26, 1998