Description: Define a function
recs  on ,
the class of ordinal
numbers, by transfinite recursion given a rule which sets the next
value given all values so far. See df-irdg 6370 for more details on why
this definition is desirable. Unlike df-irdg 6370 which restricts the
update rule to use only the previous value, this version allows the
update rule to use all previous values, which is why it is
described
as "strong", although it is actually more primitive. See tfri1d 6335 and
tfri2d 6336 for the primary contract of this definition.
(Contributed by Stefan O'Rear, 18-Jan-2015.) |