OAI/SetTheory/PartitionPrinciple/Geometry/GroundTaskBearingInsertionFulfillment.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TaskBearingMainSuccessorCode.insertion_data line 13
2. def OAI.PartitionPilot.Forcing.identityTaskCapFamily line 69
3. theorem OAI.PartitionPilot.Forcing.pair_mem_identityTaskCapFamily line 72
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.identityTaskCapFamily_mem line 89
5. theorem OAI.PartitionPilot.Forcing.GroundMainTransition.identityTaskCapFamily_function line 118
6. theorem OAI.PartitionPilot.Forcing.GroundMainTransition.identityTaskCapFamily_profile line 128
7. theorem OAI.PartitionPilot.Forcing.GroundMainTransition.identityTaskCapFamily_meet line 144
8. theorem OAI.PartitionPilot.Forcing.GroundMainTransition.identityTaskCapFamily_injection line 165
9. theorem OAI.PartitionPilot.Forcing.TaskRepresentative.identityInsertion_agreement line 193
10. theorem OAI.PartitionPilot.Forcing.GroundMainTransition.identityCompressionActor_fixes line 213
11. theorem OAI.PartitionPilot.Forcing.TaskBearingMainSuccessorCode.exists_insertionFamilies line 262