Proof of `Polynomial-time equivalence of Turing machines and word RAMs`
groundedproofs/Lax759944Proofs/TuringRamPolytimeEquivalence.lean · lax-759944
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The forward simulation covers the full current instruction set, including indexed input, input length, and EOF. The reverse simulation uses the checked instruction embedding, with both terminal-instruction costs accounted for.