OAI/SetTheory/PartitionPrinciple/Transfinite/RecursiveStateFieldEnvironments.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Forcing.RecursiveStateData line 11
  2. def OAI.PartitionPilot.Forcing.RecursiveStateData.field line 28
  3. def OAI.PartitionPilot.Forcing.RecursiveStateData.code line 31
  4. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.field_injective line 34
  5. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.code_injective line 53
  6. def OAI.PartitionPilot.Forcing.RecursiveStateData.decode line 57
  7. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.code_decode line 60
  8. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.decode_code line 63
  9. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.decode_field line 66
  10. def OAI.PartitionPilot.Forcing.recursiveStateCode line 71
  11. theorem OAI.PartitionPilot.Forcing.recursiveStateCode_inj line 74
  12. def OAI.PartitionPilot.Forcing.BoundedFormula.recursiveStateFormula line 88
  13. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_recursiveStateFormula line 92
  14. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_recursiveStateFormula line 99
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.recursiveStateData_code_mem line 116
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.recursiveStateData_field_mem line 121
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.recursiveStateData_code_mem_iff line 125
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.recursiveStateCode_mem line 131
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.recursiveStateCode_mem_iff line 151
  20. def OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.toState line 172
  21. def OAI.PartitionPilot.Forcing.RecursiveStateData.fresh line 178
  22. def OAI.PartitionPilot.Forcing.RecursiveStateData.currentCarrier line 181
  23. def OAI.PartitionPilot.Forcing.RecursiveStateData.currentOrder line 184
  24. def OAI.PartitionPilot.Forcing.RecursiveStateData.currentMeet line 190
  25. def OAI.PartitionPilot.Forcing.RecursiveStateData.successor line 193
  26. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.toState_currentCarrier line 227
  27. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.toState_currentOrder line 228
  28. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.toState_currentMeet line 229
  29. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.toState_successor line 231
  30. structure OAI.PartitionPilot.Forcing.RecursiveStateCoherence line 238
  31. theorem OAI.PartitionPilot.Forcing.RecursiveStateCoherence.refl line 258
  32. theorem OAI.PartitionPilot.Forcing.RecursiveStateCoherence.trans line 270
  33. theorem OAI.PartitionPilot.Forcing.CodedRecursiveMapInputs.next_coherent line 296
  34. def OAI.PartitionPilot.Forcing.RecursiveStateData.ofFields line 319
  35. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.ofFields_field line 323
  36. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.field_ofFields line 327
  37. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.code_ofFields line 344
  38. def OAI.PartitionPilot.Forcing.RecursiveStateData.successorEnvironment line 348
  39. def OAI.PartitionPilot.Forcing.RecursiveStateData.successorCodeFromEnvironment line 353
  40. theorem OAI.PartitionPilot.Forcing.RecursiveStateData.successorCodeFromEnvironment_spec line 358