Structural Induction
lComplementary approach to correctness.
lInduction on data values or structure.
lResembles classical
mathematical induction
lProves PC + termination at the same time.
lUseful for functional programs.
ldue to McCarthy
transformation, this means all programs
lSet-up can be trickier.