Add to ORKGIf there truly is a proof that shows that no universal halt decider exists on the basis that certain tuples: (H, Wm, W) are undecidable, then this very same proof (implemented as a Turing machine) could be used by H to reject some of its inputs. When-so-ever the hypothetical halt decider cannot derive a formal proof from its input strings and initial state to final states corresponding the mathematical logic functions of Halts(Wm, W) or Loops(Wm, W), halting undecidability has been decided