We often want to concatenate two strings and : put one of them at the end of another. is not a string according to the inductive definition of Σ^*, but we can define a function that produces that string (which we will then abbreviate as ).
There are at least two options. We could use induction on the second argument:
We could also define inductively on the pair of arguments:
Here, we have used substructure of .
in the definition of ; this is ok because can be considered a
If substructures of and respectively, then , and can all be considered substructures of : they must all have been shown to be in before we could show that .
We might be tempted to use induction on the first argument, but we fail: how do we define cat, we can only form strings using the two rules given in the inductive definition of .
in terms of and ? You might propose something like , but this is undefined for a number of reasons: (not ), so is undefined. Moreover, if we could just stick a string at the end of another string (in this case, appending to ), we wouldn't need to define ! Without first defining