OAI/SetTheory/PartitionPrinciple/Transfinite/MainPrefixSelectedTraceLaws.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.OrdinalRecursionTrace.mainPrefix_values line 13
  2. theorem OAI.PartitionPilot.Forcing.OrdinalRecursionTrace.mainPrefix_extends line 18
  3. theorem OAI.PartitionPilot.Forcing.OrdinalRecursionTrace.preservedMainPrefixHistory line 28
  4. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.unionCode_ground line 48
  5. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.ranked_union_candidate line 61
  6. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.union_mem_recursionPrefixes line 95
  7. theorem OAI.PartitionPilot.Forcing.MainPrefixHistoryExtends.union_code line 119
  8. theorem OAI.PartitionPilot.Forcing.OrdinalRecursionTrace.mainPrefix_successor_union line 135
  9. theorem OAI.PartitionPilot.Forcing.PreservedMainPrefixHistoryCode.exists_unique_groundUnionCode line 152
  10. def OAI.PartitionPilot.Forcing.mainPrefixTraceParams line 200
  11. def OAI.PartitionPilot.Forcing.mainPrefixRecursionFormula line 203
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mainPrefixTraceParams_ground line 209
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixRecursionFormula line 214
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mainPrefix_codeTrace line 223
  15. theorem OAI.PartitionPilot.Forcing.MainPrefixTraceStepCode.selected_of_nonzero line 241
  16. theorem OAI.PartitionPilot.Forcing.OrdinalRecursionTrace.mainPrefix_zero_entry line 253
  17. theorem OAI.PartitionPilot.Forcing.OrdinalRecursionTrace.mainPrefix_successor_entry line 260
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mainPrefixTraceStepClosure line 286
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_unique_selectedMainPrefixTrace line 347
  20. theorem OAI.PartitionPilot.Forcing.OrdinalRecursionTrace.exists_groundTerminalPrefixCode line 388
  21. theorem OAI.PartitionPilot.Forcing.OrdinalRecursionTrace.exists_groundTerminalPrefix line 426
  22. theorem OAI.PartitionPilot.Forcing.OrdinalRecursionTrace.terminalCode_ranked_candidate line 465
  23. theorem OAI.PartitionPilot.Forcing.OrdinalRecursionTrace.groundOmegaOne_terminalCode_ranked_candidate line 486