On 4/28/24 06:29, 'Thierry Arnoux' via Metamath wrote:
Maybe I would try as follows, using the seq operator instead of recs,
and the definition as an iterated 1-ary function
<https://en.wikipedia.org/wiki/Ackermann_function#Definition:_as_iterated_1-ary_function>:
I didn't try to check every step, but this looks about right.
As for the larger question of how to formalize recursive definitions,
generally via seq somehow. It can be a bit hard to get your head around
how seq is being used in a particular proof, but using seq is almost
always easier than trying to use recs or rec directly.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/c12e82d8-cfcf-4702-a56e-ff61b21cb6d5%40panix.com.
