OAI/SetTheory/PartitionPrinciple/Transfinite/RefinementBirthEnumerationFairness.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BirthLevelEnumerationCode line 11
  2. theorem OAI.PartitionPilot.Forcing.BirthLevelEnumerationCode.enumerates line 17
  3. theorem OAI.PartitionPilot.Forcing.BirthLevelEnumerationCode.idle line 34
  4. def OAI.PartitionPilot.Forcing.BoundedFormula.birthLevelEnumerationFormula line 49
  5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_birthLevelEnumerationFormula line 59
  6. def OAI.PartitionPilot.Forcing.BoundedFormula.birthLevelEnumerationEntryFormula line 84
  7. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_birthLevelEnumerationEntryFormula line 89
  8. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryForcing line 113
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_refinementHistoryForcing line 117
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryForcing_mem line 123
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryForcing_initial line 136
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryForcing_level_function line 150
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementHistoryForcing_pair_decomposition line 156
  14. def OAI.PartitionPilot.Forcing.TransitiveGround.birthLevelEnumerationRelation line 167
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_birthLevelEnumerationRelation line 172
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.birthLevelEnumerationRelation_mem line 185
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_refinementBirthLevelEnumerations line 208
  18. theorem OAI.PartitionPilot.Forcing.refinementDataHistoryIndices_subset line 278
  19. theorem OAI.PartitionPilot.Forcing.refinementDataHistoryAssignments_subset line 287
  20. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.prefix_assignments_cut line 296
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementDataHistoryCandidate_prefix line 307
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementDataHistoryCandidate_cut line 316
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementDataHistoryCandidate_splice line 331
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.birthEnumerationRange_spec line 359
  25. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.birthEnumeration_idle_iff line 396
  26. theorem OAI.PartitionPilot.Forcing.RefinementDataHistory.birthEnumeration_assignment_visit line 425