OAI/Computability/MinUncut/Games/FinalCNFOutput.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader line 11
  2. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader_eq line 14
  3. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_eq_formulaHeader line 20
  4. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_eq_clauseBits line 26
  5. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.header_append_outputStream line 45
  6. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.emitted_output_eq line 51
  7. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.reversed_accumulator_output line 60
  8. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.accumulator_length_bound line 65
  9. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowTimePolynomial line 73
  10. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowTimePolynomial_eval line 77
  11. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowTime_expanded line 82
  12. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial line 86
  13. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial_eval line 91
  14. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial_eval_expanded line 98
  15. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTime_le line 104
  16. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.table_phaseTime_le line 112
  17. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial line 120
  18. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial_eval line 124
  19. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.finalTime_le line 130
  20. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.redirectLabel line 150
  21. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.redirectCfg line 154
  22. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.redirectStmt line 158
  23. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.stepAux_redirect line 171
  24. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.chosen line 190
  25. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.chosen_length line 194
  26. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.mem_chosen line 196
  27. abbrev OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.Label line 199
  28. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.cleanupLabel line 203
  29. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.resetLabel line 206
  30. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.cleanupEntry line 208
  31. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.completedProgram line 211
  32. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.completedMachine line 219
  33. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.embeddedCfg line 230
  34. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.step_simulation line 235
  35. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.embedded_init line 254
  36. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.finalTapes_eq line 258
  37. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.haltList_eq line 268
  38. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.cleanupExecution line 274
  39. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.outputsInTime line 305
  40. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.completedTime line 337
  41. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFCleanup.completedTime_eval line 341
  42. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.emittedBytes_eq_formulaBits line 353
  43. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rawBudget_le_phaseTime line 357
  44. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.computableInPolyTime line 363