================================================================================
P9410   J.J. van Wamel
        "Inductive proofs with sets, and some applications in process algebra"


We formalise proofs by structural induction on sets, specified as an
algebraic data type.
The core idea is that the standard scheme for constructor induction can be
used for the derivation of alternative schemes. This way, considerable
flexibility can be obtained for proofs in the inductive theory for the sets.
For more general purposes we formulate a rule for `hybrid' induction,
which allows a variety of induction schemes.

A number of examples is provided, most of which contain well-known and
intuitively clear facts about sets that are nevertheless not always easy
to prove.
We also use our material on sets for proving some interesting properties
of two special processes that have sets as a parameter, specified in muCRL
style, representing generalised alternative and parallel compositions of
processes. We moreover demonstrate how our generalised parallel composition
can be used for a specification of broadcasting.