Go backward to Typing RulesGo up to TopGo forward to Structural Induction |

Syntax rule

E ::=true|notE | E&E_{1}_{2}

- Inductive definition:
**true**is in Expression.- If E is in Expression, then so is
**not**E. - If E
and E_{1}are in Expression, then so is E_{2}&E_{1}._{2} - No other trees are in expression.

- Expression = set of trees!
- Generate all trees in stages.
`stage`= {}._{0}`stage`=_{i+1}`stage`union {_{i}**not**E | E in`stage`} union { E_{i}&E_{1}| E_{2}, E_{1}in_{2}`stage`}._{i}- Expression = union of all
`stage`with_{i}*i >= 0*.

- Any tree in Expression is constructed in a finite number of stages.

Author: Wolfgang Schreiner

Last Modification: March 26, 1998