OAI/Computability/DirectedFeedback/Games/Generator.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Hastad.SourceGenerator.prefixPolynomial line 16
  2. def OAI.DFVSGames.Foundations.Hastad.SourceGenerator.timePolynomial line 19
  3. def OAI.DFVSGames.Foundations.Hastad.SourceGenerator.beforeFinish line 23
  4. def OAI.DFVSGames.Foundations.Hastad.SourceGenerator.enterFinishInTime line 27
  5. def OAI.DFVSGames.Foundations.Hastad.SourceGenerator.prefixInTime line 44
  6. theorem OAI.DFVSGames.Foundations.Hastad.SourceGenerator.output_empty line 60
  7. theorem OAI.DFVSGames.Foundations.Hastad.SourceGenerator.halted_configuration line 67
  8. def OAI.DFVSGames.Foundations.Hastad.SourceGenerator.outputInTime line 87
  9. def OAI.DFVSGames.Foundations.Hastad.SourceGenerator.computableInPolyTime line 123
  10. theorem OAI.DFVSGames.Foundations.Hastad.SourceGenerator.finite_work_alphabets line 140
  11. def OAI.DFVSGames.Foundations.Hastad.SourceGenerator.forErrorComputableInPolyTime line 146
  12. theorem OAI.DFVSGames.Foundations.Hastad.SourceGenerator.forError_finite_work_alphabets line 154
  13. structure OAI.DFVSGames.Foundations.PCP.ConstraintGraph line 166
  14. def OAI.DFVSGames.Foundations.PCP.ConstraintGraph.head line 177
  15. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.head_reverse line 179
  16. def OAI.DFVSGames.Foundations.PCP.ConstraintGraph.edgeSatisfied line 183
  17. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.edgeSatisfied_reverse line 186
  18. def OAI.DFVSGames.Foundations.PCP.ConstraintGraph.Satisfiable line 192
  19. def OAI.DFVSGames.Foundations.PCP.ConstraintGraph.rejectedDarts line 195
  20. def OAI.DFVSGames.Foundations.PCP.ConstraintGraph.rejectionCount line 198
  21. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.mem_rejectedDarts line 201
  22. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.rejectionCount_le line 206
  23. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.rejected_exists_of_not_satisfiable line 210
  24. theorem OAI.DFVSGames.Foundations.PCP.ConstraintGraph.rejectionCount_positive line 222
  25. abbrev OAI.DFVSGames.Foundations.PCP.GraphTables.Label line 236
  26. abbrev OAI.DFVSGames.Foundations.PCP.GraphTables.RelationTable line 237
  27. def OAI.DFVSGames.Foundations.PCP.GraphTables.relationIndex line 239
  28. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.relationIndex_val line 241
  29. def OAI.DFVSGames.Foundations.PCP.GraphTables.relationAt line 244
  30. def OAI.DFVSGames.Foundations.PCP.GraphTables.relationOf line 247
  31. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.relationAt_relationOf line 250
  32. structure OAI.DFVSGames.Foundations.PCP.GraphTables.DartRow line 254
  33. abbrev OAI.DFVSGames.Foundations.PCP.GraphTables.Rows line 259
  34. def OAI.DFVSGames.Foundations.PCP.GraphTables.reverseAt line 261
  35. def OAI.DFVSGames.Foundations.PCP.GraphTables.acceptsAt line 264
  36. def OAI.DFVSGames.Foundations.PCP.GraphTables.Valid line 267
  37. instance OAI.DFVSGames.Foundations.PCP.GraphTables.(instance at line 271) line 271
  38. structure OAI.DFVSGames.Foundations.PCP.GraphTables.Table line 275
  39. def OAI.DFVSGames.Foundations.PCP.GraphTables.rowList line 281
  40. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.rowList_length line 283
  41. def OAI.DFVSGames.Foundations.PCP.GraphTables.semantics line 286
  42. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.semantics_reverse line 297
  43. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.semantics_tail line 300
  44. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.semantics_accepts line 303
  45. def OAI.DFVSGames.Foundations.PCP.GraphTables.graphRows line 306
  46. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.reverseAt_graphRows line 309
  47. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.acceptsAt_graphRows line 314
  48. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.graphRows_valid line 319
  49. def OAI.DFVSGames.Foundations.PCP.GraphTables.ofGraph line 327
  50. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.semantics_ofGraph_reverse line 330
  51. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.semantics_ofGraph_tail line 335
  52. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.semantics_ofGraph_accepts line 341
  53. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.semantics_ofGraph_edgeSatisfied line 346
  54. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.constraintGraph_ext_inline_GraphTables line 351
  55. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.semantics_ofGraph line 365
  56. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.semantics_ofGraph_rejectionCount line 374
  57. def OAI.DFVSGames.Foundations.PCP.GraphTables.enumeratedGraph line 380
  58. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.enumeratedGraph_edgeSatisfied line 396
  59. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.enumeratedGraph_rejectionCount line 404
  60. def OAI.DFVSGames.Foundations.PCP.GraphTables.ofEnumeratedGraph line 416
  61. def OAI.DFVSGames.Foundations.PCP.GraphTables.bitWord line 420
  62. def OAI.DFVSGames.Foundations.PCP.GraphTables.parseBit line 422
  63. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.parseBit_bitWord line 427
  64. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.parseBits_bitWords line 430
  65. def OAI.DFVSGames.Foundations.PCP.GraphTables.relationWords line 436
  66. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.relationWords_length line 438
  67. def OAI.DFVSGames.Foundations.PCP.GraphTables.parseRelation line 441
  68. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.parseRelation_encoded line 447
  69. def OAI.DFVSGames.Foundations.PCP.GraphTables.rowWords line 454
  70. def OAI.DFVSGames.Foundations.PCP.GraphTables.parseRow line 457
  71. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.parseRow_encoded line 465
  72. def OAI.DFVSGames.Foundations.PCP.GraphTables.parseRows line 473
  73. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.parseRows_encoded line 481
  74. def OAI.DFVSGames.Foundations.PCP.GraphTables.tableWords line 487
  75. def OAI.DFVSGames.Foundations.PCP.GraphTables.tableBits line 490
  76. def OAI.DFVSGames.Foundations.PCP.GraphTables.decodeTableWords line 492
  77. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.decodeTableWords_encoded line 503
  78. def OAI.DFVSGames.Foundations.PCP.GraphTables.decodeTableBits line 511
  79. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.decodeTableBits_encoded line 514
  80. def OAI.DFVSGames.Foundations.PCP.GraphTables.encoding line 518
  81. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.tableBits_injective line 523
  82. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.rowWords_length line 525
  83. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.rowsWords_length line 528
  84. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.tableWords_length line 534
  85. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.tableWords_length_le_bits line 539
  86. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.relationBits_length_le line 544
  87. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.rowBits_length_le line 552
  88. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.rowsBits_length_le line 561
  89. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.tableBits_length_le line 571
  90. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.vertices_le_tableBits_length line 580
  91. theorem OAI.DFVSGames.Foundations.PCP.GraphTables.darts_le_tableBits_length line 586
  92. structure OAI.DFVSGames.Foundations.PCP.PoweringWalks.PortGraph line 596
  93. abbrev OAI.DFVSGames.Foundations.PCP.PoweringWalks.Edge line 600
  94. abbrev OAI.DFVSGames.Foundations.PCP.PoweringWalks.Walk line 601
  95. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.next line 605
  96. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.rot_rot line 607
  97. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.walkEnd line 610
  98. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.walkEnd_nil line 614
  99. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.walkEnd_cons line 616
  100. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.walkEnd_append line 619
  101. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.splitHead line 625
  102. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.rotateHead line 636
  103. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.rotateHead_vertex line 640
  104. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.rotateHead_zero line 643
  105. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.rotateHead_succ line 646
  106. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.permutePorts line 650
  107. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.wordEnd line 664
  108. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.endpoint line 668
  109. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.natCard_walk line 671
  110. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.headTailEquiv line 675
  111. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.advanceTail line 686
  112. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.edgeAt line 689
  113. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.pivotEquiv line 695
  114. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.pivotEquiv_fst line 705
  115. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.edgeAt_port line 719
  116. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.pivotEquiv_zero_apply line 735
  117. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.pivotEquiv_succ_apply line 739
  118. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.projectedFiberEquiv line 746
  119. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.projectedEventEquiv line 758
  120. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.natCard_edgeAt_fiber line 776
  121. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.natCard_edgeAt_event line 785
  122. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.leftFromPivot line 795
  123. def OAI.DFVSGames.Foundations.PCP.PoweringWalks.rightFromPivot line 801
  124. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.leftFromPivot_zero line 808
  125. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.rightFromPivot_zero line 812
  126. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.leftFromPivot_actual line 817
  127. theorem OAI.DFVSGames.Foundations.PCP.PoweringWalks.rightFromPivot_actual line 836