Deriving some expansion theorems for nonlinear functional equations by an algorithm (Q1101202)

We define the class of quasi-bilinear forms which covers the most important part of classes of nonlinear forms in functional programming. We give an algorithm for expanding such forms by equivalent transformations. We prove the corresponding theorem which guarantees that the output of the algorithm is an expansion of the input equation. And we give some examples to illustrate how to apply the algorithm to prove expansion theorems for some nonlinear equations.