OAI/Computability/WitnessedChoice/TreeElimination.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WitnessedChoice.BGS.FiniteIteration.run line 18
  2. lemma OAI.WitnessedChoice.BGS.FiniteIteration.run_subset line 22
  3. lemma OAI.WitnessedChoice.BGS.FiniteIteration.run_step line 28
  4. lemma OAI.WitnessedChoice.BGS.FiniteIteration.run_comparison line 31
  5. lemma OAI.WitnessedChoice.BGS.FiniteIteration.exists_stationary line 41
  6. lemma OAI.WitnessedChoice.BGS.FiniteIteration.run_stationary_after line 51
  7. lemma OAI.WitnessedChoice.BGS.FiniteIteration.run_fixed line 61
  8. lemma OAI.WitnessedChoice.BGS.FiniteIteration.run_least line 68
  9. lemma OAI.WitnessedChoice.BGS.TC_ofFinset_mono line 76
  10. theorem OAI.WitnessedChoice.BGS.ordinaryIteration_finite line 81
  11. abbrev OAI.WitnessedChoice.BGS.BFS.Item line 156
  12. def OAI.WitnessedChoice.BGS.BFS.update line 158
  13. lemma OAI.WitnessedChoice.BGS.BFS.mem_update line 163
  14. lemma OAI.WitnessedChoice.BGS.BFS.update_inflationary line 168
  15. lemma OAI.WitnessedChoice.BGS.BFS.update_mono line 172
  16. def OAI.WitnessedChoice.BGS.BFS.closure line 179
  17. lemma OAI.WitnessedChoice.BGS.BFS.closure_fixed line 182
  18. lemma OAI.WitnessedChoice.BGS.BFS.closure_nil line 186
  19. lemma OAI.WitnessedChoice.BGS.BFS.closure_step line 190
  20. def OAI.WitnessedChoice.BGS.BFS.good line 196
  21. lemma OAI.WitnessedChoice.BGS.BFS.update_good line 199
  22. lemma OAI.WitnessedChoice.BGS.BFS.closure_sound line 216
  23. lemma OAI.WitnessedChoice.BGS.BFS.closure_walk line 219
  24. lemma OAI.WitnessedChoice.BGS.BFS.closure_pad line 228
  25. lemma OAI.WitnessedChoice.BGS.BFS.mem_closure_iff line 238
  26. lemma OAI.WitnessedChoice.BGS.BFS.closure_reachable line 249
  27. theorem OAI.WitnessedChoice.BGS.iterationLoop_stationary line 273
  28. theorem OAI.WitnessedChoice.BGS.ordinaryIteration_stationary line 305
  29. theorem OAI.WitnessedChoice.BGS.ordinaryIteration_encoded line 323
  30. def OAI.WitnessedChoice.BGS.QuotedTerm.HFTriple line 364
  31. lemma OAI.WitnessedChoice.BGS.QuotedTerm.HFTriple_injective line 367
  32. lemma OAI.WitnessedChoice.BGS.QuotedTerm.mem_distanceBase line 371
  33. lemma OAI.WitnessedChoice.BGS.QuotedTerm.mem_distanceFresh line 376
  34. def OAI.WitnessedChoice.BGS.blockIncident line 404
  35. def OAI.WitnessedChoice.BGS.blockAdjacent line 407
  36. def OAI.WitnessedChoice.BGS.distanceCode line 410
  37. lemma OAI.WitnessedChoice.BGS.distanceCode_injective line 414
  38. lemma OAI.WitnessedChoice.BGS.ordinal_mem_elements line 424
  39. lemma OAI.WitnessedChoice.BGS.distanceStep_encoded line 430
  40. theorem OAI.WitnessedChoice.BGS.CPTTerm.distance_value line 512
  41. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_allFin line 550
  42. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_anyList line 554
  43. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_anyFin line 560
  44. lemma OAI.WitnessedChoice.BGS.coded_closure_mem line 568
  45. lemma OAI.WitnessedChoice.BGS.coded_closure_mem_dist line 583
  46. theorem OAI.WitnessedChoice.BGS.QuotedTerm.meaning_distanceAt line 600
  47. def OAI.WitnessedChoice.BGS.QuotedTerm.firstHF line 668
  48. def OAI.WitnessedChoice.BGS.QuotedTerm.secondHF line 671
  49. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_fst line 676
  50. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_snd line 680
  51. lemma OAI.WitnessedChoice.BGS.QuotedTerm.firstHF_pair line 684
  52. lemma OAI.WitnessedChoice.BGS.QuotedTerm.secondHF_pair line 689
  53. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_fst_of_eq line 694
  54. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_snd_of_eq line 698
  55. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_component_tuple line 702
  56. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_component_ofFn line 714
  57. structure OAI.WitnessedChoice.TreeTest.RootedTree line 734
  58. def OAI.WitnessedChoice.TreeTest.RootedTree.Adj line 744
  59. theorem OAI.WitnessedChoice.TreeTest.RootedTree.adj_symm line 747
  60. theorem OAI.WitnessedChoice.TreeTest.RootedTree.parent_adj line 749
  61. def OAI.WitnessedChoice.TreeTest.RootedTree.label line 755
  62. lemma OAI.WitnessedChoice.TreeTest.RootedTree.label_parent line 765
  63. theorem OAI.WitnessedChoice.TreeTest.RootedTree.exists_labels line 772
  64. structure OAI.WitnessedChoice.TreeTest.Problem line 787
  65. def OAI.WitnessedChoice.TreeTest.Problem.update line 801
  66. def OAI.WitnessedChoice.TreeTest.Problem.run line 805
  67. lemma OAI.WitnessedChoice.TreeTest.Problem.le_update line 809
  68. lemma OAI.WitnessedChoice.TreeTest.Problem.update_subset line 811
  69. lemma OAI.WitnessedChoice.TreeTest.Problem.run_subset line 814
  70. lemma OAI.WitnessedChoice.TreeTest.Problem.run_step line 819
  71. lemma OAI.WitnessedChoice.TreeTest.Problem.run_comparison line 821
  72. lemma OAI.WitnessedChoice.TreeTest.Problem.exists_stationary line 831
  73. lemma OAI.WitnessedChoice.TreeTest.Problem.run_stationary_after line 839
  74. def OAI.WitnessedChoice.TreeTest.Problem.deleted line 850
  75. lemma OAI.WitnessedChoice.TreeTest.Problem.deleted_fixed line 852
  76. def OAI.WitnessedChoice.TreeTest.Problem.survivors line 858
  77. lemma OAI.WitnessedChoice.TreeTest.Problem.mem_survivors line 860
  78. lemma OAI.WitnessedChoice.TreeTest.Problem.survival_allowed line 863
  79. lemma OAI.WitnessedChoice.TreeTest.Problem.survival_support line 871
  80. def OAI.WitnessedChoice.TreeTest.Problem.Solution line 883
  81. lemma OAI.WitnessedChoice.TreeTest.Problem.solution_survives line 887
  82. theorem OAI.WitnessedChoice.TreeTest.Problem.all_survive_iff_solution line 902