OAI/SetTheory/PartitionPrinciple/Transfinite/MainPrefixHistoryUnionRecognition.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Forcing.MainPrefixGraphFamily line 11
  2. def OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.indexUnion line 24
  3. def OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.stageUnion line 25
  4. def OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.transitionUnion line 26
  5. def OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.code line 28
  6. def OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.unionCode line 31
  7. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.indexUnion_mem line 34
  8. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.stageUnion_mem line 37
  9. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.transitionUnion_mem line 40
  10. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.indexUnion_ordinal line 44
  11. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.common_upper line 51
  12. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.chronologyPairs_indexUnion_mem line 63
  13. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.stageUnion_function line 79
  14. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.transitionUnion_function line 94
  15. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.stageUnion_restrict line 112
  16. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.transitionUnion_restrict line 120
  17. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.union_valid line 128
  18. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.unionCode_valid line 158
  19. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.fieldFamilies_ground line 181
  20. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.fieldRanges_ground line 194
  21. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.fieldUnions_ground line 202
  22. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.unionCode_ground line 207
  23. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.code_extends_union line 212
  24. def OAI.PartitionPilot.Forcing.MainPrefixProfileGraphCode line 226
  25. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.linked_profile_code line 240
  26. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.profile_graph_code line 247
  27. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.preservesOldProfiles_of_graph_code line 259
  28. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.preservesOldProfiles_iff_graph_code line 276
  29. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.union_profile_graph_code line 293
  30. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.exists_preservedUnionPrefix line 307
  31. def OAI.PartitionPilot.Forcing.PreservedMainPrefixCode line 343
  32. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixCode.valid line 350
  33. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixCode.exists_decodedPrefix line 355
  34. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.preserved_code line 388
  35. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.preserved_code_iff line 392
  36. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixProfileGraphFormula line 412
  37. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixProfileGraphFormula line 432
  38. structure OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode line 484
  39. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.exists_fields line 498
  40. def OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.fields line 508
  41. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.fields_spec line 511
  42. def OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.graphFamily line 519
  43. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.graphFamily_code_entry line 532
  44. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.graphFamily_codeGraph_eq line 540
  45. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.graphFamily_profiles line 545
  46. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.graphFamily_indexUnion line 550
  47. def OAI.PartitionPilot.Forcing.MainPrefixHistoryFieldMem line 572
  48. def OAI.PartitionPilot.Forcing.MainPrefixHistoryUnionCode line 576
  49. theorem OAI.PartitionPilot.Forcing.MainPrefixHistoryUnionCode.unique line 581
  50. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.field_mem_iff line 594
  51. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.union_code line 615
  52. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixHistoryFieldMemFormula line 638
  53. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mainPrefixHistoryFieldMem_ground line 652
  54. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixHistoryFieldMemFormula line 660
  55. def OAI.PartitionPilot.Forcing.MainPrefixAtIndex line 701
  56. def OAI.PartitionPilot.Forcing.MainPrefixHistoryExtends line 704
  57. def OAI.PartitionPilot.Forcing.MainPrefixTraceStepCode line 707
  58. theorem OAI.PartitionPilot.Forcing.MainPrefixAtIndex.unique line 712
  59. theorem OAI.PartitionPilot.Forcing.MainPrefixAtIndex.refl line 718
  60. theorem OAI.PartitionPilot.Forcing.MainPrefixTraceStepCode.unique line 723
  61. theorem OAI.PartitionPilot.Forcing.MainPrefixHistoryExtends.trans line 736
  62. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixHistoryFieldUnionFormula line 750
  63. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixHistoryUnionFormula line 753
  64. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixHistoryFieldUnionFormula line 764
  65. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixHistoryUnionFormula line 789