OAI/Computability/DirectedFeedback/Machines/FinalCNFTime.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowTimePolynomial line 10
  2. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowTimePolynomial_eval line 14
  3. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowTime_expanded line 19
  4. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial line 23
  5. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial_eval line 28
  6. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial_eval_expanded line 35
  7. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTime_le line 41
  8. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.table_phaseTime_le line 49
  9. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial line 57
  10. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial_eval line 61
  11. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.finalTime_le line 67
  12. def OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.redirectLabel line 87
  13. def OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.redirectCfg line 91
  14. def OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.redirectStmt line 95
  15. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.stepAux_redirect line 108
  16. def OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.chosen line 127
  17. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.chosen_length line 131
  18. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.mem_chosen line 133
  19. abbrev OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.Label line 136
  20. def OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.cleanupLabel line 140
  21. def OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.resetLabel line 143
  22. def OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.cleanupEntry line 145
  23. def OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.completedProgram line 148
  24. def OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.completedMachine line 156
  25. def OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.embeddedCfg line 167
  26. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.step_simulation line 172
  27. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.embedded_init line 191
  28. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.finalTapes_eq line 195
  29. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.haltList_eq line 205
  30. def OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.cleanupExecution line 211
  31. def OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.outputsInTime line 245
  32. def OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.completedTime line 277
  33. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFCleanup.completedTime_eval line 281
  34. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.emittedBytes_eq_formulaBits line 293
  35. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rawBudget_le_phaseTime line 297
  36. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.computableInPolyTime line 303
  37. def OAI.DFVSGames.Foundations.Complexity.MachineTableIteration.finalTable line 344
  38. def OAI.DFVSGames.Foundations.Complexity.MachineTableIteration.counterCertificate line 347
  39. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableIteration.countedBudget_le line 355
  40. def OAI.DFVSGames.Foundations.Complexity.MachineTableIteration.countedExecution line 381
  41. def OAI.DFVSGames.Foundations.Complexity.MachineTableIteration.outputsInTime_mono line 395
  42. def OAI.DFVSGames.Foundations.Complexity.MachineTableIteration.countedCertificate line 403
  43. def OAI.DFVSGames.Foundations.Complexity.MachineTableIteration.computableInPolyTime line 412
  44. def OAI.DFVSGames.Foundations.Complexity.MachineTableIteration.initialCertificate line 416
  45. def OAI.DFVSGames.Foundations.Complexity.MachineTableIteration.tableCertificate line 422
  46. def OAI.DFVSGames.Foundations.Complexity.MachineTableIteration.gapMapCertificate line 429
  47. theorem OAI.DFVSGames.Foundations.Complexity.TableIterationFiniteAlphabet.initial line 441
  48. theorem OAI.DFVSGames.Foundations.Complexity.TableIterationFiniteAlphabet.finalCNF line 446
  49. theorem OAI.DFVSGames.Foundations.Complexity.TableIterationFiniteAlphabet.counter line 451
  50. theorem OAI.DFVSGames.Foundations.Complexity.TableIterationFiniteAlphabet.counted line 463
  51. theorem OAI.DFVSGames.Foundations.Complexity.TableIterationFiniteAlphabet.iteration line 466
  52. theorem OAI.DFVSGames.Foundations.Complexity.TableIterationFiniteAlphabet.table line 470
  53. theorem OAI.DFVSGames.Foundations.Complexity.TableIterationFiniteAlphabet.gapMap line 474
  54. structure OAI.DFVSGames.Reduction.Incidence.Triple line 484
  55. def OAI.DFVSGames.Reduction.Incidence.parity line 490
  56. def OAI.DFVSGames.Reduction.Incidence.matchingSlots line 492
  57. def OAI.DFVSGames.Reduction.Incidence.acceptedSlots line 497
  58. def OAI.DFVSGames.Reduction.Incidence.failedEquation line 500
  59. def OAI.DFVSGames.Reduction.Incidence.bestResponse line 503
  60. theorem OAI.DFVSGames.Reduction.Incidence.local_count_bound line 506
  61. theorem OAI.DFVSGames.Reduction.Incidence.best_response_exact line 513
  62. structure OAI.DFVSGames.Reduction.Incidence.Equation line 518
  63. inductive OAI.DFVSGames.Reduction.Incidence.Slot line 526
  64. def OAI.DFVSGames.Reduction.Incidence.nameAt line 532
  65. def OAI.DFVSGames.Reduction.Incidence.bitAt line 537
  66. def OAI.DFVSGames.Reduction.Incidence.questionPredicate line 542
  67. theorem OAI.DFVSGames.Reduction.Incidence.question_predicate_at_slot line 549
  68. def OAI.DFVSGames.Reduction.Incidence.bobTriple line 558
  69. def OAI.DFVSGames.Reduction.Incidence.acceptedCount line 561
  70. def OAI.DFVSGames.Reduction.Incidence.failureCount line 568
  71. theorem OAI.DFVSGames.Reduction.Incidence.total_count_bound line 575
  72. def OAI.DFVSGames.Reduction.Incidence.optimalAlice line 586
  73. theorem OAI.DFVSGames.Reduction.Incidence.optimal_alice_exact line 590
  74. theorem OAI.DFVSGames.Reduction.Incidence.fixed_bob_optimum line 601
  75. theorem OAI.DFVSGames.Reduction.Incidence.soundness_191_over_192 line 615
  76. theorem OAI.DFVSGames.Reduction.Incidence.game_soundness_191_over_192 line 622
  77. def OAI.DFVSGames.Reduction.SourceIncidence.toIncidence line 637
  78. theorem OAI.DFVSGames.Reduction.SourceIncidence.failedEquation_eq line 640
  79. theorem OAI.DFVSGames.Reduction.SourceIncidence.failureCount_eq line 647
  80. def OAI.DFVSGames.Reduction.SourceIncidence.occurrenceList line 657
  81. theorem OAI.DFVSGames.Reduction.SourceIncidence.cloned_occurrence_gap line 660
  82. theorem OAI.DFVSGames.Reduction.SourceIncidence.source_to_incidence_soundness line 679