I have a comment re Juergen's paper: I seems to me that it is necessary to prove that EOM's and GTM's have internal logic that is both complete and consistent.
If there is no applicable decision procedure then EOM's and GTM's, it seems to me, can act as independent sources of true noise in their output without regard to the structure of the program they happen to be running. I think the proof would have to be more than just an inspection or functional demonstration of the logic system. I am far from an expert in these matters and wonder if this has merit. Hal
