OAI/Computability/WitnessedChoice/TreeCorrection.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WitnessedSeparation.Grid.edgeActionRelation line 14
  2. lemma OAI.WitnessedSeparation.Grid.mem_edgeActionRelation line 18
  3. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_cycleY_move line 35
  4. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.exists_edgeCode line 69
  5. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_cycleY line 79
  6. def OAI.WitnessedSeparation.Grid.configActionRelation line 129
  7. lemma OAI.WitnessedSeparation.Grid.mem_configActionRelation line 133
  8. lemma OAI.WitnessedSeparation.Grid.edge_config_union line 144
  9. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.exists_vertexBlockCode line 174
  10. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.all_edgeBlockCode line 184
  11. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.pair_atoms_relationCode line 194
  12. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_cycleX line 198
  13. def OAI.WitnessedSeparation.Grid.oppositeVertex line 265
  14. lemma OAI.WitnessedSeparation.Grid.dist_opposite_tail line 267
  15. lemma OAI.WitnessedSeparation.Grid.ParentEdges.flow_zero line 279
  16. lemma OAI.WitnessedSeparation.Grid.ParentEdges.flow_neg_one line 283
  17. lemma OAI.WitnessedSeparation.Grid.ParentEdges.traverses_iff_neg_nonzero line 288
  18. lemma OAI.WitnessedSeparation.Grid.ParentEdges.opposite_directed_flow_iff line 292
  19. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_reverseCycleY_move line 337
  20. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_reverseCycleY line 371
  21. abbrev OAI.WitnessedSeparation.Grid.VertexKey line 421
  22. def OAI.WitnessedSeparation.Grid.vertexKey line 423
  23. def OAI.WitnessedSeparation.Grid.lowEnd line 425
  24. def OAI.WitnessedSeparation.Grid.highEnd line 428
  25. def OAI.WitnessedSeparation.Grid.edgeKey line 431
  26. lemma OAI.WitnessedSeparation.Grid.low_high_endpoints line 434
  27. lemma OAI.WitnessedSeparation.Grid.low_lt_high line 440
  28. lemma OAI.WitnessedSeparation.Grid.ordered_endpoints_iff line 449
  29. lemma OAI.WitnessedSeparation.Grid.edgeKey_injective line 463
  30. def OAI.WitnessedSeparation.Grid.leastEdges line 478
  31. lemma OAI.WitnessedSeparation.Grid.leastEdges_empty_iff line 481
  32. lemma OAI.WitnessedSeparation.Grid.leastEdges_subsingleton line 501
  33. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_edgeLt line 526
  34. def OAI.WitnessedSeparation.Grid.missingEdge line 603
  35. def OAI.WitnessedSeparation.Grid.remainingEdges line 606
  36. lemma OAI.WitnessedSeparation.Grid.selected_inter_empty line 609
  37. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_nextEdges line 626
  38. def OAI.WitnessedSeparation.Grid.gridCandidates line 693
  39. lemma OAI.WitnessedSeparation.Grid.mem_gridCandidates line 697
  40. lemma OAI.WitnessedSeparation.Grid.candidate_new_edge line 702
  41. lemma OAI.WitnessedSeparation.Grid.gridCandidates_fresh line 709
  42. lemma OAI.WitnessedSeparation.Grid.consistent_empty line 713
  43. lemma OAI.WitnessedSeparation.Grid.consistent_insert line 716
  44. lemma OAI.WitnessedSeparation.Grid.selectedVectors_accepts line 735
  45. lemma OAI.WitnessedSeparation.Grid.gridCandidates_empty_iff line 741
  46. lemma OAI.WitnessedSeparation.Grid.remaining_empty_iff line 760
  47. lemma OAI.WitnessedSeparation.Grid.actionPerm_edgeBlock line 782
  48. lemma OAI.WitnessedSeparation.Grid.actionPerm_vertexBlock line 791
  49. lemma OAI.WitnessedSeparation.Grid.actionPerm_blocks line 800
  50. def OAI.WitnessedSeparation.Grid.ParentEdges.fundamentalPool line 815
  51. lemma OAI.WitnessedSeparation.Grid.ParentEdges.fundamental_mem line 818
  52. lemma OAI.WitnessedSeparation.Grid.ParentEdges.grid_transitivity line 822
  53. def OAI.WitnessedSeparation.Grid.edgeState line 878
  54. lemma OAI.WitnessedSeparation.Grid.edgeState_empty line 880
  55. lemma OAI.WitnessedSeparation.Grid.edgeState_insert line 882
  56. lemma OAI.WitnessedSeparation.Grid.edgeState_injective line 885
  57. lemma OAI.WitnessedSeparation.Grid.mem_edgeState line 888
  58. lemma OAI.WitnessedSeparation.Grid.ParentEdges.prefix_invariant line 895
  59. lemma OAI.WitnessedSeparation.Grid.ParentEdges.terminal_complete line 927
  60. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.meaning_cycleRelation_of_Y line 981
  61. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.cycleRelations_mem line 992
  62. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.cycleRelations_identity line 1045
  63. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.cycleRelations_positive line 1052
  64. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.cycleRelations_negative line 1071
  65. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.fundamentalPool_in_cycles line 1090
  66. lemma OAI.WitnessedSeparation.Grid.edgeAtoms_grid line 1127
  67. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.mem_value_candidates line 1144
  68. lemma OAI.WitnessedSeparation.Grid.QuotedGrid.selection_candidates line 1168