Example 2:
The Structural induction principle generalises to operate over a number of domains simultaneously. We can prove properties of two or more domains that are defined in terms of one another.
For BNF rules:
show that all S-values have an even number of occurrences of
the* token.