OAI/SetTheory/PartitionPrinciple/Transfinite/GroundInitialCompressionHistory.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_pairCompositions line 19
  2. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_pairPushFilters line 29
  3. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_recursiveSeparators line 39
  4. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_recursiveAction line 48
  5. def OAI.PartitionPilot.Forcing.RecursiveStateData.iterate line 71
  6. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.iterate_zero line 76
  7. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.iterate_succ line 79
  8. def OAI.PartitionPilot.Forcing.GroundCompressionState.next line 97
  9. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.next_data line 100
  10. def OAI.PartitionPilot.Forcing.GroundCompressionState.iterate line 105
  11. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.iterate_data line 109
  12. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.canonical_iterate_code_mem line 120
  13. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.canonical_iterate_valid line 126
  14. theorem OAI.PartitionPilot.Forcing.pairSecondField_constant line 138
  15. structure OAI.PartitionPilot.Forcing.RecursiveTemplateConstancy line 159
  16. theorem OAI.PartitionPilot.Forcing.RecursiveTemplateConstancy.space_entry_iff line 169
  17. theorem OAI.PartitionPilot.Forcing.RecursiveTemplateConstancy.relation_entry_iff line 173
  18. theorem OAI.PartitionPilot.Forcing.RecursiveTemplateConstancy.meet_entry_iff line 177
  19. theorem OAI.PartitionPilot.Forcing.RecursiveTemplateConstancy.successor line 181
  20. theorem OAI.PartitionPilot.Forcing.RecursiveTemplateConstancy.iterate line 196
  21. def OAI.PartitionPilot.Forcing.SetFormula.decodedSuccessorFormula line 212
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_decodedSuccessorFormula line 224
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_recursiveSuccessorCode line 267
  24. def OAI.PartitionPilot.Forcing.TransitiveGround.recursiveSuccessorTerm line 303
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.recursiveSuccessorTerm_eval line 368
  26. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_recursiveSuccessorCode line 373
  27. def OAI.PartitionPilot.Forcing.TransitiveGround.compressionSuccessorFormula line 385
  28. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_groundHistory line 399
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialCompressionHistory line 447