MATH.4:4.1 - State the input construction and wanted result

Name the input family, its constructors and any fixed parameters. For natural numbers, the constructors are zero and successor. A finite binary tree can be a leaf or a new root joining two smaller trees. The supplied constructor and constituents determine which recursive clause applies. If different constructions are later identified, retain that identification as a separate condition.

For each input x, state the kind of output y and the property P(x,y) it must satisfy. Include bounds or retained information that the next use consumes. For division by a positive integer d, the output is a pair (q,r) satisfying n=q*d+r and 0≤r<d.

Use the input’s actual formation rules to choose the cases. A proof about trees cannot be applied to a structure with additional edges without considering those edges.