OAI/SetTheory/PartitionPrinciple/Definability/TaskRepresentativeCodes.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.actionSectionEntryFormula line 12
  2. def OAI.PartitionPilot.Forcing.BoundedFormula.actionSectionFormula line 16
  3. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_actionSectionEntryFormula line 23
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_actionSectionFormula line 31
  5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.actionSectionEntry_correct line 41
  6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.actionSection_correct line 59
  7. def OAI.PartitionPilot.Forcing.BoundedFormula.meetFilterFormula line 95
  8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_meetFilterFormula line 105
  9. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_meetFilterFormula line 120
  10. def OAI.PartitionPilot.Forcing.BoundedFormula.restrictedActionEntryFormula line 127
  11. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_restrictedActionEntryFormula line 132
  12. def OAI.PartitionPilot.Forcing.BoundedFormula.restrictedActionFormula line 141
  13. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_restrictedActionFormula line 150
  14. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_restrictedActionFormula line 159
  15. structure OAI.PartitionPilot.Forcing.EligibleTaskCode line 171
  16. def OAI.PartitionPilot.Forcing.BoundedFormula.eligibleTaskFormula line 185
  17. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_eligibleTaskFormula line 193
  18. def OAI.PartitionPilot.Forcing.eligibleTaskSet line 209
  19. theorem OAI.PartitionPilot.Forcing.eligibleTaskSet_subset line 214
  20. theorem OAI.PartitionPilot.Forcing.mem_eligibleTaskSet line 218
  21. theorem OAI.PartitionPilot.Forcing.literalTaskCode_mem_eligibleTaskSet line 229
  22. def OAI.PartitionPilot.Forcing.BoundedFormula.eligibleTaskEntryFormula line 245
  23. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_eligibleTaskEntryFormula line 252
  24. def OAI.PartitionPilot.Forcing.TaskRepresentative line 269
  25. theorem OAI.PartitionPilot.Forcing.TaskRepresentative.restriction line 273
  26. def OAI.PartitionPilot.Forcing.taskRepresentativeRelation line 280
  27. theorem OAI.PartitionPilot.Forcing.pair_mem_taskRepresentativeRelation line 284
  28. theorem OAI.PartitionPilot.Forcing.eligibleTask_representative_total line 295
  29. def OAI.PartitionPilot.Forcing.BoundedFormula.taskRepresentativeFormula line 310
  30. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_taskRepresentativeFormula line 317
  31. def OAI.PartitionPilot.Forcing.BoundedFormula.taskRepresentativeEntryFormula line 325
  32. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_taskRepresentativeEntryFormula line 330