How do we know what the proof by simulation does in exp(g(n)) symbols, if the length of our argument is linear in n?
Exhibiting the complete proof by simulation is not necessary, I think. It’s enough to prove that it exists, that its length is bounded, and that it must contradict the proof found by R. All these statements have simple proofs by inspection of R.
How do we know what the proof by simulation does in exp(g(n)) symbols, if the length of our argument is linear in n?
Exhibiting the complete proof by simulation is not necessary, I think. It’s enough to prove that it exists, that its length is bounded, and that it must contradict the proof found by R. All these statements have simple proofs by inspection of R.