OAI/Computability/DirectedFeedback/Machines/RuntimeFinish.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.Label line 15
  2. abbrev OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.Tapes line 16
  3. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.entry line 18
  4. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.statement line 21
  5. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.canonicalTapes line 30
  6. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.finishCost line 33
  7. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.cleared_frame line 36
  8. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.reversed_tapes line 40
  9. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.finishInTime line 57
  10. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.finishCost_le_list line 117
  11. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.totalLength line 128
  12. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.totalLength_erase line 130
  13. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.drain_conservation line 144
  14. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.cleared_totalLength line 156
  15. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeFinish.finishCost_eq_totalLength line 174
  16. abbrev OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.Alphabet line 197
  17. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.finish line 199
  18. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.scan line 202
  19. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.seed line 212
  20. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.tapes line 216
  21. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_source line 220
  22. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_scratch line 226
  23. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_destination line 231
  24. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.update_source_inline_MachineUnaryAffineAt line 236
  25. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.update_scratch_inline_MachineUnaryAffineAt line 250
  26. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.update_destination_inline_MachineUnaryAffineAt line 261
  27. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.prepend_replicate_word line 267
  28. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.scan_step_succ line 272
  29. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.scan_step_zero line 292
  30. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.scanTrace line 309
  31. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.restoreTapes line 339
  32. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.affineTrace line 358
  33. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.affineInTime line 394
  34. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.seededAffineTrace line 414
  35. inductive OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.Label line 448
  36. instance OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.instFintypeLabel line 452
  37. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.program line 457
  38. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryAffineAt.machine line 463
  39. inductive OAI.DFVSGames.Explicit.MachineUniformProgram.Tape line 482
  40. instance OAI.DFVSGames.Explicit.MachineUniformProgram.instFintypeTape line 487
  41. abbrev OAI.DFVSGames.Explicit.MachineUniformProgram.State line 493
  42. def OAI.DFVSGames.Explicit.MachineUniformProgram.initialState line 495
  43. def OAI.DFVSGames.Explicit.MachineUniformProgram.headerField line 497
  44. def OAI.DFVSGames.Explicit.MachineUniformProgram.emitField line 502
  45. def OAI.DFVSGames.Explicit.MachineUniformProgram.tokens line 508
  46. def OAI.DFVSGames.Explicit.MachineUniformProgram.clearKeys line 511
  47. inductive OAI.DFVSGames.Explicit.MachineUniformProgram.Label line 515
  48. def OAI.DFVSGames.Explicit.MachineUniformProgram.headerNext line 524
  49. def OAI.DFVSGames.Explicit.MachineUniformProgram.emitEntry line 527
  50. def OAI.DFVSGames.Explicit.MachineUniformProgram.program line 530
  51. def OAI.DFVSGames.Explicit.MachineUniformProgram.machine line 546
  52. theorem OAI.DFVSGames.Explicit.MachineUniformProgram.covers line 557
  53. theorem OAI.DFVSGames.Explicit.MachineUniformProgram.accumulator_not_mem_clearKeys line 561
  54. theorem OAI.DFVSGames.Explicit.MachineUniformProgram.output_not_mem_clearKeys line 562
  55. def OAI.DFVSGames.Explicit.MachineUniformHeaders.inputTapes line 574
  56. def OAI.DFVSGames.Explicit.MachineUniformHeaders.afterVertices line 577
  57. def OAI.DFVSGames.Explicit.MachineUniformHeaders.afterAlphabet line 580
  58. def OAI.DFVSGames.Explicit.MachineUniformHeaders.resultTapes line 584
  59. theorem OAI.DFVSGames.Explicit.MachineUniformHeaders.initList_eq line 589
  60. theorem OAI.DFVSGames.Explicit.MachineUniformHeaders.first_result line 595
  61. theorem OAI.DFVSGames.Explicit.MachineUniformHeaders.second_result line 603
  62. theorem OAI.DFVSGames.Explicit.MachineUniformHeaders.third_result line 611
  63. def OAI.DFVSGames.Explicit.MachineUniformHeaders.headersInTime line 619
  64. theorem OAI.DFVSGames.Explicit.MachineUniformHeaders.headers_budget line 656
  65. def OAI.DFVSGames.Integration.GapSemantics.errorValue line 669
  66. def OAI.DFVSGames.Integration.GapSemantics.satisfactionRate line 671
  67. theorem OAI.DFVSGames.Integration.GapSemantics.countSatisfied_eq_sum line 674
  68. theorem OAI.DFVSGames.Integration.GapSemantics.countSatisfied_ofFn line 682
  69. def OAI.DFVSGames.Integration.GapSemantics.uniformConstraintAcceptance line 689
  70. theorem OAI.DFVSGames.Integration.GapSemantics.uniformConstraintAcceptance_eq_rate line 694
  71. theorem OAI.DFVSGames.Integration.GapSemantics.errorValue_pos line 705
  72. theorem OAI.DFVSGames.Integration.GapSemantics.errorValue_lt_half line 710
  73. theorem OAI.DFVSGames.Integration.GapSemantics.satisfactionRate_nonneg line 717
  74. theorem OAI.DFVSGames.Integration.GapSemantics.satisfactionRate_le_one line 721
  75. theorem OAI.DFVSGames.Integration.GapSemantics.completeAt_iff line 729
  76. theorem OAI.DFVSGames.Integration.GapSemantics.soundAt_iff line 754
  77. theorem OAI.DFVSGames.Integration.GapSemantics.completeAt_mono line 774
  78. theorem OAI.DFVSGames.Integration.GapSemantics.soundAt_mono line 780
  79. theorem OAI.DFVSGames.Integration.GapSemantics.completeAt_iff_real line 786
  80. theorem OAI.DFVSGames.Integration.GapSemantics.soundAt_iff_real line 797