OAI/SetTheory/PartitionPrinciple/Transfinite/GroundLinkedMainStageCodeLaws.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.serializedChronologyCode line 12
  2. theorem OAI.PartitionPilot.Forcing.GroundSerializedChronology.code_eq_literal line 17
  3. theorem OAI.PartitionPilot.Forcing.SerializedChronologyCode.toGround_code line 22
  4. def OAI.PartitionPilot.Forcing.BoundedFormula.serializedChronologyTupleFormula line 31
  5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_serializedChronologyTupleFormula line 36
  6. def OAI.PartitionPilot.Forcing.chronologyCandidateGraphs line 64
  7. def OAI.PartitionPilot.Forcing.SetFormula.serializedChronologyCandidateFormula line 69
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_serializedChronologyCandidateFormula_raw line 87
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_serializedChronologyCandidateFormula line 132
  10. def OAI.PartitionPilot.Forcing.TransitiveGround.serializedChronologyCandidates line 168
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_serializedChronologyCandidates line 172
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.serializedChronologyCandidates_mem line 176
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.serializedChronology_code_mem_candidates line 197
  14. def OAI.PartitionPilot.Forcing.linkedChronologyGraphs line 204
  15. def OAI.PartitionPilot.Forcing.LinkedMainStageRawCode line 207
  16. def OAI.PartitionPilot.Forcing.BoundedFormula.linkedMainStageTupleFormula line 222
  17. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_linkedMainStageTupleFormula line 225
  18. def OAI.PartitionPilot.Forcing.BoundedFormula.linkedTerminalFormula line 236
  19. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_linkedTerminalFormula line 241
  20. def OAI.PartitionPilot.Forcing.SetFormula.linkedMainStageRawFormula line 255
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_linkedMainStageRawFormula line 270
  22. theorem OAI.PartitionPilot.Forcing.LinkedMainStageRawCode.exists_linked line 321
  23. def OAI.PartitionPilot.Forcing.GroundLinkedMainStage.rawFields line 372
  24. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.rawFields_ground line 375
  25. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.rawFields_graphs line 379
  26. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.rawFields_code line 384
  27. theorem OAI.PartitionPilot.Forcing.LinkedMainStageRawCode.fields_unique line 408
  28. theorem OAI.PartitionPilot.Forcing.LinkedMainStageRawCode.exists_linked_fields line 420
  29. structure OAI.PartitionPilot.Forcing.GroundLinkedMainStage.SameCode line 442
  30. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.same_code line 449
  31. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.SameCode.field_bound line 463
  32. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.SameCode.layer_bound line 466
  33. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.SameCode.layers line 469
  34. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.SameCode.serial_values line 472
  35. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.SameCode.history_values line 485
  36. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.SameCode.birth line 493
  37. theorem OAI.PartitionPilot.Forcing.GroundLinkedMainStage.SameCode.history_five line 497