OAI/Computability/WitnessedChoice/CycleTranslation.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WitnessedChoice.BGS.QuotedTerm.mem_tupleProduct_image line 15
  2. lemma OAI.WitnessedSeparation.Grid.endpoints_incident_iff line 40
  3. def OAI.WitnessedSeparation.Grid.frameCode line 53
  4. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.next4_eq_add line 63
  5. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.prev4_eq_add line 65
  6. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.adjacent_index_iff line 67
  7. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_fv_pair line 73
  8. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_fe_pair line 80
  9. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_faceDescription line 87
  10. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.mem_faces line 124
  11. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_hasEndpoints line 168
  12. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_tree line 180
  13. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_tripleDomain line 254
  14. def OAI.WitnessedChoice.BGS.SourceProgram.cost line 275
  15. def OAI.WitnessedChoice.BGS.SourceProgram.polynomial line 280
  16. lemma OAI.WitnessedChoice.BGS.SourceProgram.resource_polynomial line 282
  17. lemma OAI.WitnessedChoice.BGS.SourceProgram.resource_basic line 289
  18. structure OAI.WitnessedSeparation.Grid.GridResources line 309
  19. lemma OAI.WitnessedSeparation.Grid.gridResources line 315
  20. lemma OAI.WitnessedSeparation.Grid.mem_edgeCode_iff line 351
  21. lemma OAI.WitnessedSeparation.Grid.mem_vertexCode_iff line 360
  22. lemma OAI.WitnessedSeparation.Grid.exists_edgeCode line 369
  23. lemma OAI.WitnessedSeparation.Grid.exists_vertexCode line 378
  24. lemma OAI.WitnessedSeparation.Grid.atom_mem_edgeCode line 387
  25. lemma OAI.WitnessedSeparation.Grid.input_inc_iff line 396
  26. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_adjacentMatch line 414
  27. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_matchFace line 434
  28. lemma OAI.WitnessedSeparation.Grid.edgeGraph_erase line 468
  29. lemma OAI.WitnessedSeparation.Grid.cut_cover line 484
  30. def OAI.WitnessedSeparation.Grid.ParentEdges.cut line 511
  31. lemma OAI.WitnessedSeparation.Grid.ParentEdges.cut_separated line 513
  32. lemma OAI.WitnessedSeparation.Grid.ParentEdges.cut_reachable_iff line 519
  33. def OAI.WitnessedSeparation.Grid.ParentEdges.cutIndicator line 532
  34. lemma OAI.WitnessedSeparation.Grid.ParentEdges.cutIndicator_head line 535
  35. lemma OAI.WitnessedSeparation.Grid.ParentEdges.cutIndicator_tail line 538
  36. lemma OAI.WitnessedSeparation.Grid.ParentEdges.cutIndicator_eq line 541
  37. lemma OAI.WitnessedSeparation.Grid.ParentEdges.cut_gradient_self line 547
  38. lemma OAI.WitnessedSeparation.Grid.ParentEdges.cut_gradient_other line 551
  39. lemma OAI.WitnessedSeparation.Grid.ParentEdges.flow_cut line 556
  40. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_connected line 593
  41. def OAI.WitnessedSeparation.Grid.distancesCode line 627
  42. def OAI.WitnessedSeparation.Grid.connTableCode line 630
  43. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_connWithout line 639
  44. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.value_distance_edges line 683
  45. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.value_distances line 693
  46. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.value_connTable line 700
  47. def OAI.WitnessedSeparation.Grid.Traverses line 742
  48. def OAI.WitnessedSeparation.Grid.traversalCode line 750
  49. lemma OAI.WitnessedSeparation.Grid.mem_traversalCode line 755
  50. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_traversal line 767
  51. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_side line 835
  52. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_onSide line 844
  53. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_matchFace_atoms line 853
  54. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_baseEq line 864
  55. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_acceptsFaces line 883
  56. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.mem_candidates line 908
  57. def OAI.WitnessedSeparation.Grid.originVertex line 941
  58. lemma OAI.WitnessedSeparation.Grid.dist_origin_head line 943
  59. lemma OAI.WitnessedSeparation.Grid.exists_traversalCode line 948
  60. lemma OAI.WitnessedSeparation.Grid.input_z_iff line 959
  61. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_traversalEdge line 975
  62. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_directedZ line 989
  63. lemma OAI.WitnessedSeparation.Grid.ParentEdges.cut_reachable_tail_iff line 1072
  64. lemma OAI.WitnessedSeparation.Grid.ParentEdges.cut_reachable_head_iff line 1082
  65. lemma OAI.WitnessedSeparation.Grid.ParentEdges.traverses_forward line 1086
  66. lemma OAI.WitnessedSeparation.Grid.ParentEdges.traverses_reverse line 1109
  67. lemma OAI.WitnessedSeparation.Grid.ParentEdges.traverses_endpoints line 1131
  68. lemma OAI.WitnessedSeparation.Grid.scalar_cases line 1152
  69. lemma OAI.WitnessedSeparation.Grid.ParentEdges.traverses_iff_nonzero line 1162
  70. lemma OAI.WitnessedSeparation.Grid.ParentEdges.directed_flow_iff line 1175
  71. lemma OAI.WitnessedSeparation.Grid.local_central_iff line 1202