Syntax rule
E ::= true | not E | E_1&E_2
- Inductive definition:
- true is in Expression.
- If E is in Expression, then so is not E.
- If E_1 and E_2 are in Expression, then so is E_1&E_2.
- No other trees are in expression.
- Expression = set of trees!
- Generate all trees in stages.
- stage_0 = {}.
- stage_{i+1} = stage_i union {
not E | E in stage_i} union { E_1&E_2
| E_1, E_2 in stage_i}.
- Expression = union of all
stage_i with i >=0.
- Any tree in Expression is constructed in a finite number of stages.
