Re: HHH(DD) does correctly reject its input as non-halting --- VERIFIED FACT +++

On 6/14/25 9:58 AM, olcott wrote:

On 6/13/2025 5:51 AM, Mikko wrote:

On 2025-06-12 15:30:05 +0000, olcott said:
>

int DD()
{
   int Halt_Status = HHH(DD);
   if (Halt_Status)
     HERE: goto HERE;
   return Halt_Status;
}
>
It is a verified fact that DD() *is* one of the forms
of the counter-example input as such an input would
be encoded in C. Christopher Strachey wrote his in CPL.
>
// rec routine P
//   §L :if T[P] go to L
//     Return §
// https://academic.oup.com/comjnl/article/7/4/313/354243
void Strachey_P()
{
   L: if (HHH(Strachey_P)) goto L;
   return;
}
>
https://academic.oup.com/comjnl/article-abstract/7/4/313/354243? redirectedFrom=fulltext

>
Strachey only informally presents the idea of the proof. Formalism
and details needed in a rigorous proof is not shown.
>

It *is* a verified fact DD correctly simulated by HHH
cannot possibly reach its own "return" statement
final halt state.

>
That "cannot possibly" is not a part of any verifiable fact as
it is not sufficiently well-defined for a verification. What
cannot be stated cearly and unambiguoulsy cannot be a verified
fact.
>

 void DDD()
{
   HHH(DDD);
   return;
}
 _DDD()
[00002192] 55             push ebp
[00002193] 8bec           mov ebp,esp
[00002195] 6892210000     push 00002192
[0000219a] e833f4ffff     call 000015d2  // call HHH
[0000219f] 83c404         add esp,+04
[000021a2] 5d             pop ebp
[000021a3] c3             ret
Size in bytes:(0018) [000021a3]
 It is a self-evidently true verified fact that DDD
correctly emulated by HHH cannot possibly reach its
own simulated "ret" instruction final halt state in
1 to ∞ steps of correct emulation of DDD by HHH.
 Everyone that does not agree has less than a first
year CS student's understanding of the C programming
language.
 

Since your HHH doesn't correctly simulate its input, and no other HHH can exists since you have changed your stipulation, and not include the code of HHH as part of the input (since you just accused me of lying and having to have corrected me when I pointed out that you have stipulated that the input doesn't contain the code for HHH).
Since the code for the HHH that aborts and returns in included in DDD, since that is the HHH that you say exists, and all HHH just look at the DDD that calls them, that must be the only one in existance, and thus your criteria is just a false statement, as that HHH doesn't correctly simulate its input, since it stops short.
Sorry, you are just boxxing yourself in by your changing lies, and proving you don't really know what you are talking about.