OAI/Computability/DirectedFeedback/RankGraph/UnweightedIntegrated.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectedFeedback.CyclicWalk line 9
  2. theorem OAI.DirectedFeedback.cyclicWalk_contains_cycle line 12
  3. def OAI.DirectedFeedback.FeedbackR line 67
  4. theorem OAI.DirectedFeedback.feedback_hits_walk line 71
  5. abbrev OAI.DirectedFeedback.Clone line 79
  6. def OAI.DirectedFeedback.cloneRel line 81
  7. def OAI.DirectedFeedback.cloneSet line 84
  8. theorem OAI.DirectedFeedback.mem_cloneSet line 87
  9. theorem OAI.DirectedFeedback.card_cloneSet line 91
  10. def OAI.DirectedFeedback.fullClusters line 95
  11. theorem OAI.DirectedFeedback.mem_fullClusters line 99
  12. theorem OAI.DirectedFeedback.cloneSet_feedback line 104
  13. theorem OAI.DirectedFeedback.fullClusters_feedback line 111
  14. theorem OAI.DirectedFeedback.cloneSet_fullClusters_subset line 129
  15. theorem OAI.DirectedFeedback.fullClusters_cost_le line 134
  16. theorem OAI.DirectedFeedback.clone_feedback_iff line 139
  17. def OAI.DirectedFeedback.roundCopies line 150
  18. theorem OAI.DirectedFeedback.roundCopies_pos line 152
  19. theorem OAI.DirectedFeedback.weighted_cost_le_copies line 157
  20. theorem OAI.DirectedFeedback.copies_cost_le line 165
  21. theorem OAI.DirectedFeedback.rounded_clone_completeness line 176
  22. theorem OAI.DirectedFeedback.rounded_clone_soundness line 190
  23. theorem OAI.DirectedFeedback.rounded_clone_size line 203
  24. abbrev OAI.DirectedFeedback.RankGraph.Tuple line 227
  25. abbrev OAI.DirectedFeedback.RankGraph.Domain line 230
  26. instance OAI.DirectedFeedback.RankGraph.(instance at line 234) line 234
  27. instance OAI.DirectedFeedback.RankGraph.(instance at line 239) line 239
  28. abbrev OAI.DirectedFeedback.RankGraph.Formal line 244
  29. inductive OAI.DirectedFeedback.RankGraph.PrefixStep line 246
  30. abbrev OAI.DirectedFeedback.RankGraph.Rank line 258
  31. instance OAI.DirectedFeedback.RankGraph.(instance at line 260) line 260
  32. def OAI.DirectedFeedback.RankGraph.vertex line 269
  33. def OAI.DirectedFeedback.RankGraph.labels line 272
  34. def OAI.DirectedFeedback.RankGraph.eval line 277
  35. theorem OAI.DirectedFeedback.RankGraph.eval_vertex line 282
  36. def OAI.DirectedFeedback.RankGraph.Arc line 286
  37. theorem OAI.DirectedFeedback.RankGraph.eval_arc line 290
  38. theorem OAI.DirectedFeedback.RankGraph.arc_irrefl line 295
  39. def OAI.DirectedFeedback.RankGraph.emptyTuple line 300
  40. def OAI.DirectedFeedback.RankGraph.marker line 302
  41. theorem OAI.DirectedFeedback.RankGraph.eval_marker line 304
  42. theorem OAI.DirectedFeedback.RankGraph.marker_injective line 307
  43. theorem OAI.DirectedFeedback.RankGraph.marker_arc line 313
  44. theorem OAI.DirectedFeedback.RankGraph.prefix_big line 317
  45. theorem OAI.DirectedFeedback.RankGraph.prefix_small line 323
  46. theorem OAI.DirectedFeedback.RankGraph.constant_pure line 329
  47. theorem OAI.DirectedFeedback.RankGraph.constant_vertex line 340
  48. def OAI.DirectedFeedback.RankGraph.twoLevel line 356
  49. def OAI.DirectedFeedback.RankGraph.compareBit line 361
  50. def OAI.DirectedFeedback.RankGraph.usable line 365
  51. def OAI.DirectedFeedback.RankGraph.referenceBit line 368
  52. def OAI.DirectedFeedback.RankGraph.Good line 372
  53. theorem OAI.DirectedFeedback.RankGraph.twoLevel_arc line 377
  54. theorem OAI.DirectedFeedback.RankGraph.compareBit_mono_of_arc line 393
  55. theorem OAI.DirectedFeedback.RankGraph.good_monotone line 403
  56. theorem OAI.DirectedFeedback.RankGraph.reference_empty line 416
  57. theorem OAI.DirectedFeedback.RankGraph.reference_univ line 428
  58. theorem OAI.DirectedFeedback.RankGraph.compare_prefix_big line 438
  59. theorem OAI.DirectedFeedback.RankGraph.compare_prefix_small line 446
  60. theorem OAI.DirectedFeedback.RankGraph.good_prefix_big line 454
  61. theorem OAI.DirectedFeedback.RankGraph.good_prefix_small line 462
  62. def OAI.DirectedFeedback.RankGraph.belowWildcard line 476
  63. def OAI.DirectedFeedback.RankGraph.aboveWildcard line 481
  64. theorem OAI.DirectedFeedback.RankGraph.wildcard_forcing line 488
  65. theorem OAI.DirectedFeedback.RankGraph.comparison_forcing line 553
  66. structure OAI.DirectedFeedback.TestGraph.Wildcard line 577
  67. structure OAI.DirectedFeedback.TestGraph.Comparison line 584
  68. abbrev OAI.DirectedFeedback.TestGraph.Vertex line 588
  69. inductive OAI.DirectedFeedback.TestGraph.Arc line 590
  70. theorem OAI.DirectedFeedback.TestGraph.arc_irrefl line 606
  71. def OAI.DirectedFeedback.TestGraph.LabelDeleted line 612
  72. def OAI.DirectedFeedback.TestGraph.labelPotential line 617
  73. theorem OAI.DirectedFeedback.TestGraph.labelPotential_increases line 623
  74. theorem OAI.DirectedFeedback.TestGraph.labelDeleted_feedback line 652
  75. theorem OAI.DirectedFeedback.TestGraph.wildcard_path line 671
  76. theorem OAI.DirectedFeedback.TestGraph.comparison_path line 681
  77. def OAI.DirectedFeedback.Prefix.boundary line 695
  78. def OAI.DirectedFeedback.Prefix.Transition line 697
  79. theorem OAI.DirectedFeedback.Prefix.boundary_mono line 700
  80. theorem OAI.DirectedFeedback.Prefix.boundary_zero line 703
  81. theorem OAI.DirectedFeedback.Prefix.boundary_top line 706
  82. theorem OAI.DirectedFeedback.Prefix.exists_transition line 709
  83. theorem OAI.DirectedFeedback.Prefix.transition_unique line 725
  84. def OAI.DirectedFeedback.Prefix.transition line 739
  85. theorem OAI.DirectedFeedback.Prefix.transition_spec line 743
  86. theorem OAI.DirectedFeedback.Prefix.transition_cell_nonempty line 748
  87. def OAI.DirectedFeedback.Prefix.conditionedSet line 761
  88. theorem OAI.DirectedFeedback.Prefix.conditionedSet_mono line 764
  89. theorem OAI.DirectedFeedback.Prefix.conditionedSet_empty line 771
  90. theorem OAI.DirectedFeedback.Prefix.conditionedSet_univ line 775
  91. theorem OAI.DirectedFeedback.Prefix.conditioned_properties line 782
  92. def OAI.DirectedFeedback.Prefix.refineCell line 791
  93. theorem OAI.DirectedFeedback.Prefix.refined_even_boundary line 797
  94. theorem OAI.DirectedFeedback.Prefix.refined_middle_boundary line 804
  95. theorem OAI.DirectedFeedback.Prefix.transition_refines line 813