OAI/Computability/DirectedFeedback/Encoding/ProductTarget.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Explicit.ProductTarget.fullTable line 16
  2. theorem OAI.DFVSGames.Explicit.ProductTarget.fullTable_images line 22
  3. theorem OAI.DFVSGames.Explicit.ProductTarget.permutationEquiv_fullTable line 25
  4. def OAI.DFVSGames.Explicit.ProductTarget.row line 30
  5. def OAI.DFVSGames.Explicit.ProductTarget.render line 37
  6. theorem OAI.DFVSGames.Explicit.ProductTarget.render_length line 48
  7. theorem OAI.DFVSGames.Explicit.ProductTarget.render_get line 54
  8. def OAI.DFVSGames.Explicit.ProductTarget.render_simpleBipartite line 63
  9. theorem OAI.DFVSGames.Explicit.ProductTarget.render_count line 94
  10. def OAI.DFVSGames.Explicit.ProductTarget.mergeLabelings line 112
  11. theorem OAI.DFVSGames.Explicit.ProductTarget.mergeLabelings_left line 117
  12. theorem OAI.DFVSGames.Explicit.ProductTarget.mergeLabelings_right line 123
  13. theorem OAI.DFVSGames.Explicit.ProductTarget.render_count_merge line 129
  14. theorem OAI.DFVSGames.Explicit.ProductTarget.render_maxSatisfied line 139
  15. theorem OAI.DFVSGames.Explicit.ProductTarget.render_value line 160
  16. def OAI.DFVSGames.Explicit.ProductTarget.tuples line 172
  17. theorem OAI.DFVSGames.Explicit.ProductTarget.tuples_length line 175
  18. theorem OAI.DFVSGames.Explicit.ProductTarget.tuples_mem line 178
  19. theorem OAI.DFVSGames.Explicit.ProductTarget.tuples_nodup line 182
  20. theorem OAI.DFVSGames.Explicit.ProductTarget.tuples_get line 185
  21. theorem OAI.DFVSGames.Explicit.ProductTarget.tuple_address line 190
  22. theorem OAI.DFVSGames.Explicit.ProductTarget.address_eq_ofDigits line 194
  23. theorem OAI.DFVSGames.Explicit.ProductTarget.address_eq_horner line 205
  24. def OAI.DFVSGames.Explicit.SubdivisionTarget.ofInstance line 221
  25. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.ofInstance_count line 227
  26. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.ofInstance_maxSatisfied line 237
  27. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.ofInstance_value line 247
  28. def OAI.DFVSGames.Explicit.SubdivisionTarget.numericRightEquiv line 253
  29. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.numericRightEquiv_false_val line 256
  30. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.numericRightEquiv_true_val line 261
  31. def OAI.DFVSGames.Explicit.SubdivisionTarget.numericVertexEquiv line 266
  32. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.numericVertexEquiv_original_val line 274
  33. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.numericVertexEquiv_middle_val line 277
  34. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.numericVertexEquiv_p_val line 280
  35. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.numericVertexEquiv_r_val line 285
  36. def OAI.DFVSGames.Explicit.SubdivisionTarget.numericEdgeEquiv line 290
  37. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.numericEdgeEquiv_symm_val line 293
  38. def OAI.DFVSGames.Explicit.SubdivisionTarget.tables line 298
  39. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.tables_correspond line 303
  40. def OAI.DFVSGames.Explicit.SubdivisionTarget.vertexFields line 311
  41. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.vertexFields_val line 319
  42. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.rows_eq line 326
  43. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.tables_translation line 335
  44. def OAI.DFVSGames.Explicit.SubdivisionTarget.subdivide line 354
  45. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.subdivide_vertices line 360
  46. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.subdivide_length line 363
  47. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.subdivide_translation line 367
  48. def OAI.DFVSGames.Explicit.SubdivisionTarget.simpleBipartite line 376
  49. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.numeric_side line 379
  50. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.simpleBipartite_side line 398
  51. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.subdivide_count line 402
  52. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.subdivide_value line 410
  53. theorem OAI.DFVSGames.Explicit.SubdivisionTarget.value_eq line 415
  54. theorem OAI.DFVSGames.Explicit.SubdivisionEncoding.subdivide_constraints line 430
  55. theorem OAI.DFVSGames.Explicit.SubdivisionEncoding.subdivide_constraints_flatMap line 447
  56. theorem OAI.DFVSGames.Explicit.SubdivisionEncoding.subdivide_gameWords line 454
  57. theorem OAI.DFVSGames.Explicit.SubdivisionEncoding.encodeWords_flatMap_inline_SubdivisionEncoding line 465
  58. theorem OAI.DFVSGames.Explicit.SubdivisionEncoding.subdivide_gameBits line 471
  59. theorem OAI.DFVSGames.Explicit.SubdivisionEncoding.subdivide_gameWords_length line 479
  60. theorem OAI.DFVSGames.Explicit.SubdivisionEncoding.subdivide_gameBits_length_le line 483
  61. def OAI.DFVSGames.Explicit.MachineSubdivisionCorrespondence.Involutive line 501
  62. theorem OAI.DFVSGames.Explicit.MachineSubdivisionCorrespondence.inverseTable_eq line 505
  63. theorem OAI.DFVSGames.Explicit.MachineSubdivisionCorrespondence.translations_involutive line 513
  64. theorem OAI.DFVSGames.Explicit.MachineSubdivisionCorrespondence.rowBits_eq_semantic line 534
  65. theorem OAI.DFVSGames.Explicit.MachineSubdivisionCorrespondence.outputRows_eq_ofFn line 553
  66. theorem OAI.DFVSGames.Explicit.MachineSubdivisionCorrespondence.outputRows_eq_semantic line 562
  67. theorem OAI.DFVSGames.Explicit.MachineSubdivisionCorrespondence.output_eq_gameBits line 571
  68. def OAI.DFVSGames.Explicit.MachineSubdivisionRuntime.prefixPolynomial line 591
  69. def OAI.DFVSGames.Explicit.MachineSubdivisionRuntime.timePolynomial line 596
  70. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRuntime.input_eq line 599
  71. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRuntime.input_size line 603
  72. def OAI.DFVSGames.Explicit.MachineSubdivisionRuntime.finalTapes line 610
  73. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRuntime.final_outputEmpty line 615
  74. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRuntime.final_accumulator line 617
  75. def OAI.DFVSGames.Explicit.MachineSubdivisionRuntime.prefixInTime line 623
  76. def OAI.DFVSGames.Explicit.MachineSubdivisionRuntime.fullRunInTime line 654
  77. def OAI.DFVSGames.Explicit.MachineSubdivisionRuntime.computableInPolyTime line 662
  78. def OAI.DFVSGames.Explicit.MachineSubdivisionRuntime.familyComputableInPolyTime line 678
  79. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRuntime.workAlphabetFinite line 694
  80. def OAI.DFVSGames.Explicit.MachineSubdivisionCompose.certifiedOutput line 714
  81. def OAI.DFVSGames.Explicit.MachineSubdivisionCompose.certify line 717
  82. def OAI.DFVSGames.Explicit.MachineSubdivisionCompose.computableInPolyTime line 727
  83. theorem OAI.DFVSGames.Explicit.MachineSubdivisionCompose.finiteAlphabet line 735
  84. def OAI.DFVSGames.Explicit.MachineSubdivisionCompose.translationComputableInPolyTime line 743