OAI/Computability/DirectedFeedback/Machines/PoweringRuntimeBudget.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Foundations.Complexity.PoweringRuntimeBudget.stackLength_le_of_execution line 55
  2. theorem OAI.DFVSGames.Foundations.Complexity.PoweringRuntimeBudget.stackLength_le_from_input line 65
  3. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringRuntimeBudget.tapeCount line 73
  4. theorem OAI.DFVSGames.Foundations.Complexity.PoweringRuntimeBudget.finish_steps_le_of_execution line 76
  5. theorem OAI.DFVSGames.Foundations.Complexity.PoweringRuntimeBudget.total_steps_le_of_execution line 91
  6. def OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.preBudget line 113
  7. def OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.finishBudget line 117
  8. def OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget line 122
  9. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.preBudget_mono_vertices line 127
  10. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.finishBudget_mono line 134
  11. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget_mono_vertices line 149
  12. def OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.rowTime line 158
  13. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.rowTime_eval line 165
  14. def OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.vertexTime line 171
  15. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.vertexTime_eval line 174
  16. def OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.preTime line 179
  17. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.preTime_eval line 183
  18. def OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.time line 188
  19. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.time_eval line 196
  20. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget_le_time line 202
  21. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.setup_loop_finish_le_time line 209
  22. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.execution_budget_le_time line 222
  23. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPolynomialBudget.graph_totalBudget_le_time line 235
  24. def OAI.DFVSGames.Foundations.PCP.PortTables.HasPortTails line 251
  25. instance OAI.DFVSGames.Foundations.PCP.PortTables.(instance at line 254) line 254
  26. theorem OAI.DFVSGames.Foundations.PCP.PortTables.flatRows_hasPortTails line 258
  27. def OAI.DFVSGames.Foundations.PCP.PortTables.ofRows line 262
  28. theorem OAI.DFVSGames.Foundations.PCP.PortTables.table_ext_inline_PortTableEncoding line 274
  29. theorem OAI.DFVSGames.Foundations.PCP.PortTables.ofRows_flatRows line 283
  30. def OAI.DFVSGames.Foundations.PCP.PortTables.extractInput line 293
  31. theorem OAI.DFVSGames.Foundations.PCP.PortTables.extractInput_graphTable line 305
  32. def OAI.DFVSGames.Foundations.PCP.PortTables.decodeInputBits line 309
  33. theorem OAI.DFVSGames.Foundations.PCP.PortTables.decodeInputBits_inputBits line 312
  34. def OAI.DFVSGames.Foundations.PCP.PortTables.encoding line 317
  35. theorem OAI.DFVSGames.Foundations.PCP.PortTables.inputBits_injective line 322
  36. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish line 336
  37. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.finishConfiguration line 340
  38. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinishBudget line 344
  39. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_ready line 348
  40. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_output line 356
  41. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_vertices line 367
  42. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_darts line 375
  43. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.serialized_eq line 384
  44. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinishExecution line 391
  45. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.finishSteps line 412
  46. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.finishExecution line 416
  47. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.execution line 442
  48. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.finishSteps_le line 455
  49. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.execution_budget_le line 466
  50. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime line 475
  51. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime_finite_alphabet line 497
  52. abbrev OAI.DFVSGames.Foundations.PCP.RoundComputation.PreprocessingCertificate line 513
  53. abbrev OAI.DFVSGames.Foundations.PCP.RoundComputation.PoweringCertificate line 518
  54. theorem OAI.DFVSGames.Foundations.PCP.RoundComputation.powered_eq_transform line 524
  55. def OAI.DFVSGames.Foundations.PCP.RoundComputation.poweredPolynomialTimeOfCertificates line 529
  56. def OAI.DFVSGames.Foundations.PCP.RoundComputation.tablePolynomialTimeOfCertificates line 539
  57. theorem OAI.DFVSGames.Foundations.PCP.RoundComputation.powered_finiteAlphabet line 549
  58. theorem OAI.DFVSGames.Foundations.PCP.RoundComputation.finiteAlphabet line 557
  59. def OAI.DFVSGames.Foundations.PCP.RoundComputation.tablePolynomialTime line 569
  60. theorem OAI.DFVSGames.Foundations.PCP.RoundComputation.tablePolynomialTime_finite_alphabet line 577