OAI/Computability/VertexCover/PCP/AlphabetTableEnumeration.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.bitValue line 13
  2. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv line 15
  3. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv_val line 17
  4. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.productEquiv line 20
  5. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.productEquiv_val line 24
  6. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv line 30
  7. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inl_val line 34
  8. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inr_val line 38
  9. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.tapeCount line 42
  10. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.pairTapeCount line 43
  11. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.fiveTapeCount line 44
  12. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.localCount line 45
  13. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.eventCount line 46
  14. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.addressCount line 47
  15. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.vertexCount line 48
  16. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.dartCount line 49
  17. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv line 51
  18. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.cubeRank line 54
  19. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank line 55
  20. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_cubeRank line 58
  21. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.cubeRank_cubeUnrank line 61
  22. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_digit line 64
  23. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv_val line 72
  24. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.pairIndex line 78
  25. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.pairIndex_val line 80
  26. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv line 85
  27. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank line 88
  28. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank line 91
  29. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank_pairCubeRank line 94
  30. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank_pairCubeUnrank line 97
  31. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv_val line 100
  32. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv line 105
  33. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv line 109
  34. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv line 118
  35. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv line 123
  36. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv line 127
  37. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv line 132
  38. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv line 137
  39. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv line 142
  40. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv_val line 144
  41. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv_val line 148
  42. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv_val line 153
  43. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv_val line 161
  44. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv_val line 170
  45. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inl_val line 177
  46. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inr_val line 184
  47. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_event_val line 191
  48. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_vertexAddress_val line 195
  49. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_edgeAddress_val line 202
  50. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_val line 210
  51. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_reverse_val line 218
  52. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.ordered line 224
  53. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_length line 227
  54. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.mem_ordered line 230
  55. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_nodup line 235
  56. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_refl line 240
  57. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_bool line 242
  58. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_trans_finCongr line 244
  59. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_product line 250
  60. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_sum line 266
  61. def OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.localEvents line 286
  62. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.localEvents_length line 289
  63. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_event line 292
  64. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_dart line 299
  65. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.card_cube line 310
  66. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.card_pairCube line 313
  67. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.card_localEvent line 317
  68. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.card_event line 321
  69. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.card_address line 325
  70. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.card_vertex line 329
  71. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.card_dart line 334
  72. theorem OAI.UniqueGames.Foundations.PCP.AlphabetTable.Enumeration.localCount_formula line 339