Inductively Defined Sets; Structural Induction
摘要
This chapter introduces a generalisation of the definitions by induction (recursion) of the last section. Here we define sets inductively, not functions. The associated proof tool —induction along an inductive definition, or structural induction— of properties of inductively defined sets is introduced and validated.