[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

On 2020-08-23 00:21, mechvel at scico.botik.ru wrote:
> [..]
> 
> Do you mean that you doubt in that question of "will F terminate or 
> not?"
> is already solved somewhere?
> Well, if we doubt in that the F machine can run infinitely, then very 
> naturally
> we doubt of that the above proof for the goal G is correct. Then the 
> usage of EM
> is not safe in this case.
> 
> If so, then the question of "What can be the third case" occurs 
> senseless.
> Because even the statement of the second case, "F never stops" occurs 
> senseless.


I think now in a different way about how can it look the third case
(probably similar as Guillaume wrote):

the third case is that  time or space is exhausted before it becomes 
solved whether
the machine F terminates.


Regards,

--
SM