OAI/Computability/WitnessedChoice/ChoiceTrace.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WitnessedChoice.BGS.TC_eq_familyClosure line 15
  2. lemma OAI.WitnessedChoice.BGS.descendants_TC_subset line 19
  3. lemma OAI.WitnessedChoice.BGS.descendants_TC_bound line 24
  4. lemma OAI.WitnessedChoice.BGS.TC_closed line 36
  5. lemma OAI.WitnessedChoice.BGS.TC_in_domain line 41
  6. lemma OAI.WitnessedChoice.BGS.uniform_descendants line 68
  7. lemma OAI.WitnessedChoice.BGS.descendants_count_iff line 89
  8. lemma OAI.WitnessedChoice.BGS.uniform_TC_bound line 108
  9. abbrev OAI.WitnessedChoice.BGS.Traced line 129
  10. def OAI.WitnessedChoice.BGS.tracedLoop line 131
  11. lemma OAI.WitnessedChoice.BGS.iterationLoop_traced line 200
  12. def WitnessedChoice.BGS.ClosedTrace line 282
  13. lemma WitnessedChoice.BGS.closedTrace_closure line 284
  14. lemma WitnessedChoice.BGS.closedTrace_union line 288
  15. lemma WitnessedChoice.BGS.closedTrace_biUnion line 295
  16. lemma WitnessedChoice.BGS.closedTrace_insert line 301
  17. lemma WitnessedChoice.BGS.closure_emptyHF line 308
  18. lemma WitnessedChoice.BGS.closure_unionHF_subset line 311
  19. lemma WitnessedChoice.BGS.closure_uniqueHF_subset line 323
  20. lemma WitnessedChoice.BGS.tracedLoop_closure_subset line 336
  21. lemma WitnessedChoice.BGS.tracedLoop_closed line 350
  22. lemma WitnessedChoice.BGS.Term.traced_closure line 364
  23. lemma WitnessedChoice.BGS.Term.traced_self line 397
  24. lemma WitnessedChoice.BGS.closure_eq_insert_TC line 444
  25. lemma WitnessedChoice.BGS.closure_card_le_TC line 454
  26. lemma WitnessedChoice.BGS.card_closure_atoms line 458
  27. lemma WitnessedChoice.BGS.tracedLoop_card line 478
  28. def WitnessedChoice.BGS.tracePotential line 518
  29. lemma WitnessedChoice.BGS.tracePotential_var line 521
  30. lemma WitnessedChoice.BGS.tracePotential_cons line 527