Description: Define the well-ordered recursive function generator. This function takes
the usual expressions from recursion theorems and forms a unified
definition. Specifically, given a function F , a relation R , and
a base set A , this definition generates a function
G = wrecs ( R , A , F ) that has property that, at any point
x e. A , ( Gx ) = ( F` ( G |`Pred ( R , A , x ) ) ) . See
wfr1 , wfr2 , and wfr3 . (Contributed by Scott Fenton, 7-Jun-2018)(Revised by BJ, 27-Oct-2024)