Pers,
There are many proven non-computable functions, and to prove a function has any
property, you have to be able to define it analytically. For example, the Busy
Beaver Function is non-computable, but it can be defined in ZFC, and therefore
in Metamath.
Cheers, Paul
--
You received this m
Norm wrote:
> Lest it be forgotten, another experiment that shows explicit substitutions is
> here::
> http://us.metamath.org/mpeuni/_mmbrows2p2e4.png
> This was done by Paul Chapman around 2007 I think.
> AFAIK this was just a proof of concept experiment, and he didn't pu
On 17/04/2023 12:59, Glauco wrote:
|- A. a e. NN A. b e. NN A. c e. NN A. n e. ( ZZ>= ` 3 )
( ( a ^ n ) + ( b ^ n ) ) =/= ( c ^ n )
I think I'd prefer
|- A. a e. NN A. b e. NN A. c e. NN A. n e. NN
( ( ( a ^ n ) + ( b ^ n ) ) = ( c ^ n ) -> n <= 2 )
since it shows where the cutoff occurs.
On 08/06/2023 03:54, David A. Wheeler wrote:
These verifiers were written
in different programming languages by different people in different programming
languages.
By different people. :)
Cheers, Paul
--
You received this message because you are subscribed to the Google Groups
"Metamath" g
David & Norm,
Ordered!
Cheers, Paul
--
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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
Norm & David,
Received my Metamath book today. Yay!
Didn't make it into the index. Boo!
Cheers, Paul
--
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 metamath+unsu
David & Norm,
Erratum: there's a stray right parenthesis in paragraph 3 of page 32 after
"set.mm".
Cheers, Paul
--
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 me
David,
I'm lazy. Clip my Twitter pic if you like. https://twitter.com/igblan
Cheers, Paul
--
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 metamath+unsubscr...@goog
