OAI/Computability/DirectedFeedback/Games/Product.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Explicit.BipartiteGame.product line 17
  2. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_left line 33
  3. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_right line 36
  4. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_permutation line 39
  5. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_isTranslation line 43
  6. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_edge_card line 51
  7. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_left_card line 54
  8. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_right_card line 57
  9. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_edges_nonempty line 60
  10. def OAI.DFVSGames.Explicit.BipartiteGame.toGame line 67
  11. theorem OAI.DFVSGames.Explicit.BipartiteGame.toGame_accepts_on_edge line 75
  12. theorem OAI.DFVSGames.Explicit.BipartiteGame.toGame_isProjection line 88
  13. def OAI.DFVSGames.Explicit.BipartiteGame.occurrenceSuccess line 99
  14. theorem OAI.DFVSGames.Explicit.BipartiteGame.toGame_success line 105
  15. theorem OAI.DFVSGames.Explicit.BipartiteGame.toGame_success_eq_satisfiedCount line 124
  16. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_uniform_edge_law line 137
  17. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_success_eq_repetition line 142
  18. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_coordinate_success line 173
  19. theorem OAI.DFVSGames.Explicit.BipartiteGame.one_sub_mul_one_sub_le_pow line 179
  20. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_coordinate_completeness line 190
  21. theorem OAI.DFVSGames.Explicit.BipartiteGame.toGame_value line 203
  22. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_value_eq_repetition line 217
  23. theorem OAI.DFVSGames.Explicit.BipartiteGame.product_completeness line 229
  24. def OAI.DFVSGames.Explicit.BipartiteGame.relabel line 238
  25. theorem OAI.DFVSGames.Explicit.BipartiteGame.relabel_isTranslation line 245
  26. theorem OAI.DFVSGames.Explicit.BipartiteGame.relabel_success line 259
  27. theorem OAI.DFVSGames.Explicit.BipartiteGame.relabel_success_forward line 280
  28. theorem OAI.DFVSGames.Explicit.BipartiteGame.relabel_value line 289
  29. def OAI.DFVSGames.Explicit.BipartiteGame.binaryProductEquiv line 304
  30. def OAI.DFVSGames.Explicit.BipartiteGame.binaryProduct line 316
  31. theorem OAI.DFVSGames.Explicit.BipartiteGame.binaryProduct_isTranslation line 320
  32. theorem OAI.DFVSGames.Explicit.BipartiteGame.binaryProduct_dimension_positive line 325
  33. theorem OAI.DFVSGames.Explicit.BipartiteGame.binaryProduct_alphabet_card line 328
  34. theorem OAI.DFVSGames.Explicit.BipartiteGame.binaryProduct_value_eq_repetition line 335
  35. theorem OAI.DFVSGames.Explicit.BipartiteGame.binaryProduct_completeness line 340
  36. def OAI.DFVSGames.Explicit.ProductPaddedOutput.Embedded.row line 366
  37. def OAI.DFVSGames.Explicit.ProductPaddedOutput.Embedded.render line 372
  38. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.Embedded.render_length line 382
  39. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.Embedded.render_get line 386
  40. def OAI.DFVSGames.Explicit.ProductPaddedOutput.Embedded.simpleBipartite line 394
  41. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.Embedded.count line 425
  42. def OAI.DFVSGames.Explicit.ProductPaddedOutput.Embedded.extendLabelings line 439
  43. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.Embedded.extendLabelings_left line 445
  44. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.Embedded.extendLabelings_right line 451
  45. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.Embedded.maxSatisfied line 456
  46. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.Embedded.value line 474
  47. abbrev OAI.DFVSGames.Explicit.ProductPaddedOutput.Left line 489
  48. abbrev OAI.DFVSGames.Explicit.ProductPaddedOutput.Right line 490
  49. def OAI.DFVSGames.Explicit.ProductPaddedOutput.graph line 492
  50. def OAI.DFVSGames.Explicit.ProductPaddedOutput.vertices line 497
  51. def OAI.DFVSGames.Explicit.ProductPaddedOutput.side line 529
  52. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.side_left line 532
  53. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.side_right line 539
  54. def OAI.DFVSGames.Explicit.ProductPaddedOutput.outputRow line 546
  55. def OAI.DFVSGames.Explicit.ProductPaddedOutput.output line 551
  56. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.output_vertices line 555
  57. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.output_constraints line 558
  58. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.output_length line 561
  59. def OAI.DFVSGames.Explicit.ProductPaddedOutput.simpleBipartite line 564
  60. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.outputRow_source line 568
  61. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.outputRow_target line 574
  62. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.outputRow_images line 580
  63. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.output_gameWords line 589
  64. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.output_value_eq_repetition line 597
  65. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.output_completeness line 607
  66. def OAI.DFVSGames.Explicit.ProductPaddedOutput.finalCoordinates line 618
  67. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.finalCoordinates_apply line 624
  68. theorem OAI.DFVSGames.Explicit.ProductPaddedOutput.output_translations line 629
  69. abbrev OAI.DFVSGames.Foundations.Complexity.MachineLookup.Alphabet line 660
  70. def OAI.DFVSGames.Foundations.Complexity.MachineLookup.discard line 662
  71. def OAI.DFVSGames.Foundations.Complexity.MachineLookup.select line 669
  72. inductive OAI.DFVSGames.Foundations.Complexity.MachineLookup.Label line 676
  73. instance OAI.DFVSGames.Foundations.Complexity.MachineLookup.(instance at line 680) line 680
  74. def OAI.DFVSGames.Foundations.Complexity.MachineLookup.program line 684
  75. def OAI.DFVSGames.Foundations.Complexity.MachineLookup.tapes line 693
  76. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.tapes_index line 698
  77. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.tapes_source line 704
  78. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.tapes_destination line 710
  79. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.tapes_other line 715
  80. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.update_index line 721
  81. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.update_source line 735
  82. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.update_destination line 746
  83. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.fieldTapes_eq line 752
  84. def OAI.DFVSGames.Foundations.Complexity.MachineLookup.machine line 759