Go backward to Example Go up to Top

Simultaneous Induction

S ::= *E*
E :: = +S | **

Mutually recursive definition of syntax domains.

Proposition

All S-values have an even number of * occurences.

Proof

We prove by simultaneous induction on S and E "all S-values and all E-values have an even number of * occurences".

1. *E*: number(S) = 2+number(E) which is even, since number(E) is even.
2. +S: number(E) = number(S) which is even.
3. **: number(**) = 2 which is even.