program valid
ProvedResourceScheduling.Graph.program_validalgorithmspolynomial-time
The fixed graph-reduction program obeys the syntactic loop-counter write discipline.
Preamble
import Definitions.Def_ResourceScheduling_Graph_ReductionProgram open ResourceScheduling.Graph
Formal statement
namespace ResourceScheduling.Graph theorem program_valid : GraphProgram.program.Valid := by sorry end ResourceScheduling.Graph
Source
New auxiliary formalization for the ResourceScheduling Q2 reduction. The target is the unchanged CookPvsNP one-tape machine model, following Cook, The P versus NP problem, Clay Mathematics Institute (2000), Appendix. This explicit finite-column stack compiler and its simulation lemmas are new contributions, not numbered claims from Cook or the scheduling source paper.