OAI/Computability/DirectedFeedback/Encoding/TableIteration.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.PCP.TableIteration.run line 11
  2. def OAI.DFVSGames.Foundations.PCP.TableIteration.runTables line 13
  3. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.run_val line 16
  4. def OAI.DFVSGames.Foundations.PCP.TableIteration.iterationCount line 24
  5. def OAI.DFVSGames.Foundations.PCP.TableIteration.output line 26
  6. def OAI.DFVSGames.Foundations.PCP.TableIteration.outputTable line 28
  7. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.output_val line 31
  8. def OAI.DFVSGames.Foundations.PCP.TableIteration.gapMap line 34
  9. opaque OAI.DFVSGames.Foundations.PCP.TableIteration.degreeData line 36
  10. def OAI.DFVSGames.Foundations.PCP.TableIteration.polynomialDegree line 39
  11. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.sizeFactor_le_power line 41
  12. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.run_completeness line 44
  13. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.output_completeness line 48
  14. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.gapMap_completeness line 52
  15. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.output_darts_positive line 58
  16. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.gapMap_nonempty line 62
  17. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.run_size line 65
  18. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.output_size line 69
  19. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.initial_size_le line 74
  20. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.output_size_le_input line 77
  21. def OAI.DFVSGames.Foundations.PCP.TableIteration.tableSizePolynomial line 85
  22. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.tableSizePolynomial_eval line 88
  23. def OAI.DFVSGames.Foundations.PCP.TableIteration.tableBitsPolynomial line 93
  24. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.output_bits_le line 96
  25. def OAI.DFVSGames.Foundations.PCP.TableIteration.formulaBitsPolynomial line 101
  26. theorem OAI.DFVSGames.Foundations.PCP.TableIteration.gapMap_bits_le line 104
  27. def OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.wordEquiv line 119
  28. def OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.walkEquiv line 125
  29. def OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.addressEquiv line 128
  30. def OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.labelEquiv line 134
  31. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.wordEnd_map line 146
  32. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.endpoint_map line 154
  33. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.reach_iff line 158
  34. def OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.ballEquiv line 169
  35. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.wordToBall_map line 175
  36. def OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.pullSelector line 181
  37. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.decode_pullSelector line 189
  38. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.decode_transport line 195
  39. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.opinionAt_pullSelector line 205
  40. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.advanceTail_map line 218
  41. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.edgeAt_map line 226
  42. def OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.pullAccepts line 241
  43. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.pathAccepts_map line 244
  44. def OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.dartEquiv line 270
  45. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.edgeSatisfied_map line 273
  46. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.rejectionCount_map line 286
  47. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.satisfiable_iff line 307
  48. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.pullReverse line 324
  49. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.base_edgeSatisfied_map line 330
  50. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.base_rejectionCount_map line 340
  51. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.uniform_count_gap line 368
  52. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap line 407
  53. theorem OAI.DFVSGames.Foundations.PCP.PoweringPortReindex.lazy_table_uniform_count_gap_at line 446
  54. theorem OAI.DFVSGames.Foundations.PCP.RoundTableGap.powered_count_gap line 480
  55. theorem OAI.DFVSGames.Foundations.PCP.RoundTableGap.build_count_gap line 512
  56. theorem OAI.DFVSGames.Foundations.PCP.RoundTableGap.step_gap line 527
  57. theorem OAI.DFVSGames.Foundations.PCP.TableGapReduction.run_gap line 545
  58. theorem OAI.DFVSGames.Foundations.PCP.TableGapReduction.output_gap line 550
  59. theorem OAI.DFVSGames.Foundations.PCP.TableGapReduction.output_satisfiable_iff line 558
  60. theorem OAI.DFVSGames.Foundations.PCP.TableGapReduction.gapMap_satisfiable_iff line 568
  61. theorem OAI.DFVSGames.Foundations.PCP.TableGapReduction.output_count_gap line 572
  62. theorem OAI.DFVSGames.Foundations.PCP.TableGapReduction.gapMap_clauseGap line 592
  63. theorem OAI.DFVSGames.Foundations.PCP.TableGapReduction.finalClauseGap_le_one line 598
  64. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.rowWidth line 625
  65. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.rowOffset line 627
  66. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.rowsWords_split line 629
  67. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.rowsBits_split line 638
  68. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.rowsBits_append_split line 647
  69. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.prefixWords line 656
  70. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.suffixWords line 659
  71. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.prefixWords_length line 662
  72. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.tableWords_at_row line 667
  73. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.tableBits_at_row line 676
  74. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.tableBits_header line 682
  75. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.tableWords_drop_row line 687
  76. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.tableWords_take_row line 694
  77. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_tail line 700
  78. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_reverse line 705
  79. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.tableWords_drop_relation line 710
  80. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.relationWords_get line 716
  81. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_relation line 721
  82. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_predicate line 731
  83. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.rowOffset_lt_length line 738
  84. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Input.relationOffset_lt_length line 746