OAI/SetTheory/PartitionPrinciple/Geometry/GroundFairPreparationMonotonicity.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.FairPreparationStateCode line 11
  2. def OAI.PartitionPilot.Forcing.BoundedFormula.exFairStateFields line 19
  3. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_exFairStateFields line 24
  4. def OAI.PartitionPilot.Forcing.BoundedFormula.fairPreparationStateFormula line 45
  5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_fairPreparationStateFormula line 54
  6. def OAI.PartitionPilot.Forcing.FairPreparationStepCode line 77
  7. def OAI.PartitionPilot.Forcing.BoundedFormula.insertPairFormula line 95
  8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_insertPairFormula line 99
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.activePreparationFormula line 117
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_activePreparationFormula line 126
  11. def OAI.PartitionPilot.Forcing.BoundedFormula.fairStepFieldsFormula line 142
  12. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_fairStepFieldsFormula line 156
  13. def OAI.PartitionPilot.Forcing.BoundedFormula.fairPreparationStepFormula line 175
  14. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_fairPreparationStepFormula line 182
  15. def OAI.PartitionPilot.Forcing.TransitiveGround.fairPreparationStates line 207
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_fairPreparationStates line 212
  17. def OAI.PartitionPilot.Forcing.TransitiveGround.fairPreparationTransition line 218
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_fairPreparationTransition line 225
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fairPreparationStates_mem line 244
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fairPreparationTransition_mem line 271
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteHistory_bound line 307
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_fairPreparation_initial line 316
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fairPreparationTransition_serial line 334
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundFairPreparationOrbit line 408
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.varyingPreparationRelation_strengthens line 461
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fairPreparationStep_strengthens line 473