How about using the substitution rule used in the [Metamath Proof Explorer] ? Define I() in terms of applying a description of a series of allowable substitutions, to create a new numbered F() function which is the resultant application of that series of allowable substitutions. DR : So instead of I() trying to construct a multiplication function F(2, ...) from analysing the regular changes between a series of applications of the addition function F(1, ...), you'd have some highly restricted substitution specification language that let you describe explicitly how to go from one to the other.
