# Substructure

Given an element of an inductively defined set , a substructure of is one of the "smaller" elements of that was used when creating .

Substructures are important, because they tell you what inductive assumptions you can make when proving in a proof by structural induction, and also what recursive uses of you can use when defining in an inductively defined function.

You can identify the substructures of by looking at the rule defining : each of the uses of the variable from in the rule indicates a substructure. For example, if , then the only substructure of is ; you can see this because was constructed using the rule ; this rule has a reuse of the variable from the LHS, so the corresponding part of is a substructure.

In the binary tree example, if , there are no substructures of , and the substructures of are and , since these reuse the variable from the LHS.