OAI/SetTheory/PartitionPrinciple/Forcing/CodedRecursiveTaskActions.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PartitionPilot.Forcing.SetActionCode line 11
  2. theorem OAI.PartitionPilot.Forcing.PosetActionCode.toSetAction line 18
  3. def OAI.PartitionPilot.Forcing.taggedActionGraph line 22
  4. theorem OAI.PartitionPilot.Forcing.triple_mem_taggedActionGraph line 28
  5. theorem OAI.PartitionPilot.Forcing.SetActionCode.entry_shape line 46
  6. theorem OAI.PartitionPilot.Forcing.SetActionCode.entry_unique line 53
  7. theorem OAI.PartitionPilot.Forcing.taggedActionGraph_old_iff line 62
  8. theorem OAI.PartitionPilot.Forcing.taggedActionGraph_fresh_iff line 70
  9. theorem OAI.PartitionPilot.Forcing.taggedActionGraph_fresh_pair_iff line 85
  10. theorem OAI.PartitionPilot.Forcing.taggedActionGraph_subset line 96
  11. theorem OAI.PartitionPilot.Forcing.taggedActionGraph_function line 108
  12. theorem OAI.PartitionPilot.Forcing.taggedActionGraph_one line 125
  13. theorem OAI.PartitionPilot.Forcing.taggedActionGraph_mul line 133
  14. theorem OAI.PartitionPilot.Forcing.SetActionCode.tagged line 153
  15. def OAI.PartitionPilot.Forcing.SetActionCode.rawAct line 167
  16. theorem OAI.PartitionPilot.Forcing.SetActionCode.rawAct_entry line 174
  17. theorem OAI.PartitionPilot.Forcing.SetActionCode.rawAct_eq_iff line 179
  18. def OAI.PartitionPilot.Forcing.SetActionCode.inverseActor line 188
  19. theorem OAI.PartitionPilot.Forcing.SetActionCode.inverseActor_left line 193
  20. theorem OAI.PartitionPilot.Forcing.SetActionCode.inverseActor_right line 200
  21. theorem OAI.PartitionPilot.Forcing.SetActionCode.rawAct_inverse_left line 211
  22. theorem OAI.PartitionPilot.Forcing.SetActionCode.rawAct_inverse_right line 223
  23. def OAI.PartitionPilot.Forcing.SetActionCode.toPerm line 235
  24. def OAI.PartitionPilot.Forcing.BoundedFormula.taggedActionEntryFormula line 252
  25. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_taggedActionEntryFormula line 257
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.taggedActionGraph_mem line 273
  27. structure OAI.PartitionPilot.Forcing.CodedAttachmentCovariance line 302
  28. theorem OAI.PartitionPilot.Forcing.CodedAttachmentCovariance.monotone line 313
  29. theorem OAI.PartitionPilot.Forcing.PosetActionCode.tagged_attachment line 361
  30. structure OAI.PartitionPilot.Forcing.CodedRecursiveTaskAction line 375
  31. def OAI.PartitionPilot.Forcing.CodedRecursiveTaskAction.current line 394
  32. theorem OAI.PartitionPilot.Forcing.CodedRecursiveTaskAction.current_entry line 409
  33. def OAI.PartitionPilot.Forcing.CodedRecursiveTaskAction.toTaskSymmetry line 420
  34. theorem OAI.PartitionPilot.Forcing.CodedRecursiveTaskAction.toTaskSymmetry_perm_entry line 435
  35. theorem OAI.PartitionPilot.Forcing.CodedRecursiveTaskAction.toTaskSymmetry_current_entry line 440