gallais

I think I (and others) have been pretty clear that we will not answer your question on this thread as it's off topic. We even invited you to open a separate thread. I don't know why you feel the need to 1. write an adversarial rant 2. conclude by "if you cannot or will not (...)" as if we had not been crystal clear earlier in the conversation.

As @Blaisorblade said, "what do I need to trust to accept a formal proof as valid" is a more general question that deserves its own thread. As for "fastidious", I find this adversarial reformulation of the OP's question ridiculous.

@user21820 The OP asked for a proof they could translate to Agda. This paper contains one that has been independently formalised in Coq, Beluga, F*, and Lean 3. Even if you don't trust the Agda formalisation based on sized types, it's not completely outrageous to think that's a good candidate for OP to translate to Agda without sized types.

You clearly have reading comprehension issues. I'll repeat myself: Please stop mentioning me.

@Zeta And the previous comment too. Both of which yielded bigger changes than you both advocating the use of the (partial) function foldr1. Anyway. Please stop mentioning me: I'm not interested in your continuous abuse of power to rewrite history / appropriate other people's work.

@Zeta Easy for you to deny my contribution after 200_success' vandalism has erased all of its traces. And now you're once again advocating sweeping everything under the rug. What a malignant approach to this website you have! Hope you enjoy your little pré-carré. Count me out.

@Zeta Not interested in endless bureaucracy that will lead nowhere. Thanks again for, together with 200_success, making this website a little bit worse. Every effort counts! /s

@Zeta No thanks. I'm on this website to do code reviews. Not to debate with bureaucrats who take pleasure into brutally applying asinine rules. I'll think twice about helping anyone next time.

@200_success And you are now deleting comments criticising your absurd vandalism of this question. Take a break on the power trip...

@200_success I did not answer as comments, I made simple remarks that guided Matthias towards writing his own answers by making his code better himself. Which is a far superior learning process than just having code dumped on you (although I do that too sometimes).

@200_success You have now removed the whole interaction I had with Matthias and sabotaged his post demonstrating the evolution of his code trough various suggestions. Congratulations on destroying the interactive review process. I hope your one-liner of an answer makes you happy. You exemplify a lot of the things that are wrong with the stackexchange websites: a strict adherence to a set of absurd rules which takes pride in ignoring when contributions are actually helping the OP.

That is exactly my point: how can you claim that a problem is decidable (cf. this thread's title) when you're not able to decide which one of the two algorithms is the good one?

1. Take a random Turing machine and a random input. 2. Either the computation will go on for ever or it will stop at some point and there is a (constant) computable function describing each one of these behaviors. 3. ??? 4. Profit! I feel like, following your proof scheme, one could prove that termination is decidable. Did I miss something?