OAI/Computability/StarHeight/EndSearch.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GeneralizedStarHeight.EndSearch.width line 15
  2. def OAI.GeneralizedStarHeight.EndSearch.Eligible line 17
  3. lemma OAI.GeneralizedStarHeight.EndSearch.width_bounds line 20
  4. def OAI.GeneralizedStarHeight.EndSearch.eligibleSet line 29
  5. lemma OAI.GeneralizedStarHeight.EndSearch.mem_eligibleSet line 33
  6. def OAI.GeneralizedStarHeight.EndSearch.search line 42
  7. lemma OAI.GeneralizedStarHeight.EndSearch.search_none line 46
  8. lemma OAI.GeneralizedStarHeight.EndSearch.search_some line 56
  9. lemma OAI.GeneralizedStarHeight.EndSearch.width_shift line 76
  10. lemma OAI.GeneralizedStarHeight.EndSearch.changed_eligibility line 81
  11. lemma OAI.GeneralizedStarHeight.EndSearch.crossing line 92
  12. lemma OAI.GeneralizedStarHeight.EndSearch.instability_charge line 110
  13. def OAI.GeneralizedStarHeight.EndSearch.Boundary line 139
  14. lemma OAI.GeneralizedStarHeight.EndSearch.boundary_charge_card line 142
  15. def OAI.GeneralizedStarHeight.EndSearch.Unstable line 182
  16. lemma OAI.GeneralizedStarHeight.EndSearch.unstable_card line 185
  17. lemma OAI.GeneralizedStarHeight.EndSearch.two_searches_card line 206
  18. lemma OAI.GeneralizedStarHeight.MarkerSearch.interval_card line 224
  19. lemma OAI.GeneralizedStarHeight.EndSearch.nested line 263
  20. lemma OAI.GeneralizedStarHeight.EndSearch.anchor_card line 279
  21. lemma OAI.GeneralizedStarHeight.StencilSparsity.biUnion_card_real line 317
  22. lemma OAI.GeneralizedStarHeight.StencilSparsity.whole_stencil line 328
  23. lemma OAI.GeneralizedStarHeight.StencilSparsity.good_copy line 363
  24. def OAI.GeneralizedStarHeight.StencilSparsity.decode line 378
  25. lemma OAI.GeneralizedStarHeight.StencilSparsity.decode_eq_some line 381
  26. lemma OAI.GeneralizedStarHeight.StencilSparsity.decode_sound line 398