OAI/SetTheory/PartitionPrinciple/Forcing/GroundRecursiveActions.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.taskTransportGraph_mem line 17
  2. def OAI.PartitionPilot.Forcing.TransitiveGround.groundTaskTransport line 41
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.literalTask_transport_mem line 45
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundTaskTransport_total line 65
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundTaskTransport_function line 92
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundTaskTransport_mem line 105
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundTaskTransport_one line 118
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundTaskTransport_mul line 127
  9. def OAI.PartitionPilot.Forcing.indexedTaskActionGraph line 144
  10. theorem OAI.PartitionPilot.Forcing.indexedTaskActionGraph_subset line 150
  11. theorem OAI.PartitionPilot.Forcing.mem_indexedTaskActionGraph line 154
  12. theorem OAI.PartitionPilot.Forcing.triple_mem_indexedTaskActionGraph line 171
  13. theorem OAI.PartitionPilot.Forcing.indexedTaskActionGraph_entry_iff line 185
  14. theorem OAI.PartitionPilot.Forcing.indexedTaskActionGraph_function line 199
  15. theorem OAI.PartitionPilot.Forcing.indexedTaskActionGraph_setAction line 218
  16. theorem OAI.PartitionPilot.Forcing.constantTemplateFresh_subset line 241
  17. def OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleFreshAction line 254
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundTaskTransport_setAction line 263
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEligibleFreshAction_setAction line 278
  20. def OAI.PartitionPilot.Forcing.ActionAgreementBelow line 309
  21. theorem OAI.PartitionPilot.Forcing.ActionAgreementBelow.symm line 319
  22. theorem OAI.PartitionPilot.Forcing.ActionAgreementBelow.entry_eq line 322
  23. theorem OAI.PartitionPilot.Forcing.ActionAgreementBelow.image_subset line 332
  24. theorem OAI.PartitionPilot.Forcing.ActionAgreementBelow.actionImage_eq line 351
  25. theorem OAI.PartitionPilot.Forcing.ActionAgreementBelow.postcompose_eq line 361
  26. theorem OAI.PartitionPilot.Forcing.EligibleTaskCode.base_below_positive line 377
  27. theorem OAI.PartitionPilot.Forcing.TaskTransportCode.literal_outputs line 391
  28. theorem OAI.PartitionPilot.Forcing.TaskTransportCode.positive_agreement line 403
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundTaskTransport_positive_agreement line 427
  30. def OAI.PartitionPilot.Forcing.BoundedFormula.indexedTaskActionEntryFormula line 454
  31. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_indexedTaskActionEntryFormula line 460
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedTaskActionGraph_mem line 476
  33. abbrev OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextFreshSet line 511
  34. def OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextIndexAction line 515
  35. def OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextFreshAction line 518
  36. def OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextActionGraph line 521
  37. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextFreshSet_shape line 524
  38. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextIndices_closed line 537
  39. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextIndexAction_setAction line 554
  40. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextFreshAction_setAction line 560
  41. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextAction_setAction line 568
  42. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextAction_old_iff line 572
  43. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextAction_fresh_pair_iff line 577
  44. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextFreshAction_pair_iff line 583
  45. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextFreshSet_closed line 605
  46. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextAction_fresh_entry line 618
  47. theorem OAI.PartitionPilot.Forcing.PosetActionCode.agreement_identity_iff_fixes line 635
  48. theorem OAI.PartitionPilot.Forcing.IdealEmbeddingCode.actionAgreementBelow line 660
  49. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextIndices_mem line 702
  50. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextFreshSet_mem line 711
  51. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextIndexAction_mem line 726
  52. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextFreshAction_mem line 736
  53. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextActionGraph_mem line 750