OAI/SetTheory/PartitionPrinciple/Definability/RecursiveActionRealization.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.next_upper line 16
  2. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextFresh_shadow line 34
  3. def OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextNodes line 52
  4. def OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextEncode line 58
  5. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextEncode_old line 62
  6. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextEncode_fresh line 65
  7. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextEncode_mem line 69
  8. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextNodes_injective line 73
  9. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextNodes_surjective line 87
  10. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextEncode_injective line 97
  11. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.nextEncode_surjective line 100
  12. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.next_le_encode line 107
  13. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.next_meet_entry line 138
  14. theorem OAI.PartitionPilot.Forcing.CodedRecursiveTaskAction.nextAction_entry line 164
  15. theorem OAI.PartitionPilot.Forcing.CodedRecursiveTaskAction.nextAction_entry_iff line 177
  16. theorem OAI.PartitionPilot.Forcing.CodedRecursiveTaskAction.nextAction_order_iff line 190
  17. theorem OAI.PartitionPilot.Forcing.CodedRecursiveTaskAction.nextAction_code line 204
  18. theorem OAI.PartitionPilot.Forcing.CodedRecursiveTaskAction.nextAction_map_meet line 213