Of every possible (correct or incorrect) encoding of simulating partial
halt decider H that can possibly exist H either aborts the simulation of
its input or does not abort the simulation of its input.

If the computation P(P) never halts if H never aborts its simulation of
P then we can know for sure that the computation P(P) specifies an
infinite chain of invocations that must be aborted at some point.

Premise(1) (axiom) Every computation that never halts unless its
simulation is aborted is a computation that never halts. This verified
as true on the basis of the meaning of its words.

Premise(2) (verified fact) The simulation of the input to H(P,P) never
halts without being aborted is a verified fact on the basis of its x86
execution trace. (shown below).

Conclusion(3) From the above true premises it necessarily follows that
simulating halt decider H correctly reports that its input: (P,P) never
halts.

void P(u32 x)
{ u32 Input_Halts = H(x, x);
if (Input_Halts)
HERE: goto HERE;
}

int main()
{ P((u32)P);
}

_P()
[00000b25](01) 55 push ebp
[00000b26](02) 8bec mov ebp,esp
[00000b28](01) 51 push ecx
[00000b29](03) 8b4508 mov eax,[ebp+08]
[00000b2c](01) 50 push eax
[00000b2d](03) 8b4d08 mov ecx,[ebp+08]
[00000b30](01) 51 push ecx
[00000b31](05) e81ffeffff call 00000955
[00000b36](03) 83c408 add esp,+08
[00000b39](03) 8945fc mov [ebp-04],eax
[00000b3c](04) 837dfc00 cmp dword [ebp-04],+00
[00000b40](02) 7402 jz 00000b44
[00000b42](02) ebfe jmp 00000b42
[00000b44](02) 8be5 mov esp,ebp
[00000b46](01) 5d pop ebp
[00000b47](01) c3 ret
Size in bytes:(0035) [00000b47]

_main()
[00000c05](01) 55 push ebp
[00000c06](02) 8bec mov ebp,esp
[00000c08](05) 68250b0000 push 00000b25
[00000c0d](05) e813ffffff call 00000b25
[00000c12](03) 83c404 add esp,+04
[00000c15](02) 33c0 xor eax,eax
[00000c17](01) 5d pop ebp
[00000c18](01) c3 ret
Size in bytes:(0020) [00000c18]

Columns
(1) Machine address of instruction
(2) Machine address of top of stack
(3) Value of top of stack after instruction executed
(4) Machine language bytes
(5) Assembly language text
===============================
....[00000c05][0010165e][00000000](01) 55 push ebp
....[00000c06][0010165e][00000000](02) 8bec mov ebp,esp
....[00000c08][0010165a][00000b25](05) 68250b0000 push 00000b25
....[00000c0d][00101656][00000c12](05) e813ffffff call 00000b25
....[00000b25][00101652][0010165e](01) 55 push ebp
....[00000b26][00101652][0010165e](02) 8bec mov ebp,esp
....[00000b28][0010164e][00000000](01) 51 push ecx
....[00000b29][0010164e][00000000](03) 8b4508 mov eax,[ebp+08]
....[00000b2c][0010164a][00000b25](01) 50 push eax
....[00000b2d][0010164a][00000b25](03) 8b4d08 mov ecx,[ebp+08]
....[00000b30][00101646][00000b25](01) 51 push ecx
....[00000b31][00101642][00000b36](05) e81ffeffff call 00000955

Begin Local Halt Decider Simulation at Machine Address:b25
....[00000b25][002116fe][00211702](01) 55 push ebp
....[00000b26][002116fe][00211702](02) 8bec mov ebp,esp
....[00000b28][002116fa][002016ce](01) 51 push ecx
....[00000b29][002116fa][002016ce](03) 8b4508 mov eax,[ebp+08]
....[00000b2c][002116f6][00000b25](01) 50 push eax
....[00000b2d][002116f6][00000b25](03) 8b4d08 mov ecx,[ebp+08]
....[00000b30][002116f2][00000b25](01) 51 push ecx
....[00000b31][002116ee][00000b36](05) e81ffeffff call 00000955
....[00000b25][0025c126][0025c12a](01) 55 push ebp
....[00000b26][0025c126][0025c12a](02) 8bec mov ebp,esp
....[00000b28][0025c122][0024c0f6](01) 51 push ecx
....[00000b29][0025c122][0024c0f6](03) 8b4508 mov eax,[ebp+08]
....[00000b2c][0025c11e][00000b25](01) 50 push eax
....[00000b2d][0025c11e][00000b25](03) 8b4d08 mov ecx,[ebp+08]
....[00000b30][0025c11a][00000b25](01) 51 push ecx
....[00000b31][0025c116][00000b36](05) e81ffeffff call 00000955
Local Halt Decider: Infinite Recursion Detected Simulation Stopped
....[00000b36][0010164e][00000000](03) 83c408 add esp,+08
....[00000b39][0010164e][00000000](03) 8945fc mov [ebp-04],eax
....[00000b3c][0010164e][00000000](04) 837dfc00 cmp dword
[ebp-04],+00
....[00000b40][0010164e][00000000](02) 7402 jz 00000b44
....[00000b44][00101652][0010165e](02) 8be5 mov esp,ebp
....[00000b46][00101656][00000c12](01) 5d pop ebp
....[00000b47][0010165a][00000b25](01) c3 ret
....[00000c12][0010165e][00000000](03) 83c404 add esp,+04
....[00000c15][0010165e][00000000](02) 33c0 xor eax,eax
....[00000c17][00101662][00100000](01) 5d pop ebp
....[00000c18][00101666][00000098](01) c3 ret
Number_of_User_Instructions(39)
Number of Instructions Executed(26459)

In the computation P(P) if any invocation of the infinite chain of
invocations must be aborted to prevent the infinite execution of this
chain then we know that the computation: P(P) does specify an infinite
chain of invocations.

Whenever P calls H(P,P) H must abort its simulation of P. The above
computation P(P) calls H(P,P) which is the first invocation of an
infinite sequence of invocations.

It is common knowledge that any invocation of an infinite sequence of
invocations (such as infinite recursion or infinitely nested simulation)
is terminated then the entire sequence halts.

In the computation P(P) the third element of the infinite sequence of
invocations is terminated.

The only reason that any P ever halts is that some H aborted some P.
This proves (axiomatically) that P(P) really does specify an infinite
invocation chain.

(Axiom) Every computation that never halts unless its simulation is
aborted is a computation that never halts. This verified as true on the
basis of the meaning of its words.

Halting problem undecidability and infinitely nested
https://www.researchgate.net/publication/351947980_Halting_problem_undecidability_and_infinitely_nested_simulation

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein