OAI/SetTheory/PartitionPrinciple/Geometry/GroundEligibleCaps.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.PosetActionCode.raw_fixes_top line 13
  2. theorem OAI.PartitionPilot.Forcing.EligibleTaskCode.source_proper line 26
  3. theorem OAI.PartitionPilot.Forcing.eligibleTaskBatchInputs line 50
  4. def OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTasks line 89
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTasks_mem line 92
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.literalTaskCode_mem_groundEligibleTasks line 120
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTaskFields line 139
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTaskBatchInputs line 162
  9. theorem OAI.PartitionPilot.Forcing.literalTaskBound_rank_lt line 183
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundPower_rank_lt line 193
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundRelations_rank_lt line 200
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundMeetFilters_rank_lt line 205
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTasks_rank_lt line 211
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.taskRepresentativeRelation_mem line 232
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundTaskRepresentatives line 257
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTaskAttachment line 289
  17. theorem OAI.PartitionPilot.Forcing.GroundBelow.meetFilters line 360
  18. theorem OAI.PartitionPilot.Forcing.GroundBelow.literalTaskBound line 368
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTasks_below line 387
  20. def OAI.PartitionPilot.Forcing.eligibleTaskCap line 416
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTask_cap_fresh line 428
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTask_cap_entry line 440
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTask_cap_mem line 453
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTask_cap_shadow line 459
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTask_negative_cap line 482
  26. def OAI.PartitionPilot.Forcing.initialCapGraph line 526
  27. theorem OAI.PartitionPilot.Forcing.mem_initialCapGraph line 530
  28. theorem OAI.PartitionPilot.Forcing.pair_mem_initialCapGraph line 539
  29. theorem OAI.PartitionPilot.Forcing.initialCapGraph_function line 550
  30. def OAI.PartitionPilot.Forcing.BoundedFormula.initialCapEntryFormula line 566
  31. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_initialCapEntryFormula line 571
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.initialCapGraph_mem line 586
  33. def OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTaskCaps line 609
  34. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleTaskCaps_spec line 620