OAI/SetTheory/PartitionPrinciple/Transfinite/CodedMainPrefixSystems.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.GroundChronologicalHistory.fieldValue line 17
  2. def OAI.PartitionPilot.Forcing.CompressionChronologyFields.fieldValue line 25
  3. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologyGraph line 41
  4. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologyGraph_ground line 55
  5. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.chronologyGraph_function line 65
  6. def OAI.PartitionPilot.Forcing.GroundExternalBirthData.groundChronologyFields line 74
  7. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.groundChronologyFields_graph line 80
  8. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.groundChronologyFields_values line 85
  9. theorem OAI.PartitionPilot.Forcing.GroundExternalBirthData.groundChronologyFields_code_ground line 113
  10. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.graphPrefixCode_iff_values line 125
  11. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.field_laws line 157
  12. def OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.ofFieldLaws line 170
  13. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.ofFieldLaws_map line 195
  14. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainTransition.ofFieldLaws_self line 200
  15. theorem OAI.PartitionPilot.Forcing.GroundChronologicalHistory.fieldValue_rank_lt line 215
  16. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.graph_rank_lt_of_history line 235
  17. def OAI.PartitionPilot.Forcing.GroundCompressionState.prefixGraph line 275
  18. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.prefixGraph_exact line 279
  19. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_groundPrefixFields line 305
  20. def OAI.PartitionPilot.Forcing.linkedMainStageCode line 365
  21. theorem OAI.PartitionPilot.Forcing.linkedMainStageCode_inj line 368
  22. structure OAI.PartitionPilot.Forcing.GroundLinkedMainStage line 377
  23. def OAI.PartitionPilot.Forcing.GroundLinkedMainStage.code line 389
  24. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.code_ground line 392
  25. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.terminal_values line 396
  26. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.invariant_code line 408
  27. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.code_rank_lt line 415
  28. structure OAI.PartitionPilot.Forcing.GroundMainPrefix line 435
  29. def OAI.PartitionPilot.Forcing.GroundMainPrefix.indices line 461
  30. def OAI.PartitionPilot.Forcing.GroundMainPrefix.stageGraph line 463
  31. def OAI.PartitionPilot.Forcing.GroundMainPrefix.transitionGraph line 465
  32. def OAI.PartitionPilot.Forcing.GroundMainPrefix.code line 468
  33. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.code_ground line 471
  34. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageGraph_function line 475
  35. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.transitionGraph_function line 478
  36. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageGraph_entry line 485
  37. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.transitionGraph_entry line 489
  38. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.identity_entry line 495
  39. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.composition_entry line 501
  40. theorem OAI.PartitionPilot.Forcing.GroundInitialMainSeedData.initialSerialization_agreement line 519
  41. def OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.pointSystem line 564
  42. def OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.actorSystem line 578
  43. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.common_upper line 603
  44. def OAI.PartitionPilot.Forcing.GroundMainPrefix.pointSystem line 614
  45. def OAI.PartitionPilot.Forcing.GroundMainPrefix.actorSystem line 617
  46. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointSystem_carrier line 620
  47. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointSystem_map line 623
  48. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorSystem_carrier line 626
  49. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorSystem_map line 629