OAI/ModelTheory/Choiceless/Reachability.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CPTSeparation.Interpretations.map_payload line 15
  2. theorem OAI.CPTSeparation.Interpretations.map_vertexCode line 32
  3. theorem OAI.CPTSeparation.Interpretations.map_mem_wrappers line 37
  4. theorem OAI.CPTSeparation.Interpretations.map_mem_pairFamily line 42
  5. theorem OAI.CPTSeparation.Interpretations.map_mem_classFamily line 50
  6. def OAI.CPTSeparation.Interpretations.Program.stateIso line 66
  7. def OAI.CPTSeparation.Interpretations.Program.code line 70
  8. theorem OAI.CPTSeparation.Interpretations.Program.code_injective line 74
  9. theorem OAI.CPTSeparation.Interpretations.Program.map_code line 79
  10. def OAI.CPTSeparation.Interpretations.Program.baseFamily line 87
  11. def OAI.CPTSeparation.Interpretations.Program.family line 90
  12. theorem OAI.CPTSeparation.Interpretations.Program.family_mono line 97
  13. theorem OAI.CPTSeparation.Interpretations.Program.base_subset_family line 100
  14. theorem OAI.CPTSeparation.Interpretations.Program.atom_mem_family line 105
  15. theorem OAI.CPTSeparation.Interpretations.Program.ordinal_mem_family line 108
  16. theorem OAI.CPTSeparation.Interpretations.Program.code_mem_family line 111
  17. theorem OAI.CPTSeparation.Interpretations.Program.baseFamily_transitive line 120
  18. theorem OAI.CPTSeparation.Interpretations.Program.family_transitive line 130
  19. theorem OAI.CPTSeparation.Interpretations.Program.map_mem_baseFamily line 144
  20. theorem OAI.CPTSeparation.Interpretations.Program.map_mem_family line 152
  21. theorem OAI.CPTSeparation.Interpretations.Program.baseFamily_card_le line 175
  22. theorem OAI.CPTSeparation.Interpretations.Program.family_card_le line 182
  23. theorem OAI.CPTSeparation.Interpretations.Program.trace_family line 212
  24. def OAI.CPTSeparation.Interpretations.Formula.scopedWidth line 230
  25. theorem OAI.CPTSeparation.Interpretations.Formula.context_le_width line 239
  26. def OAI.CPTSeparation.Interpretations.guardedEquiv line 249
  27. theorem OAI.CPTSeparation.Interpretations.count_comparison line 261
  28. theorem OAI.CPTSeparation.Interpretations.uniform_translate line 297
  29. def OAI.CPTSeparation.Reachability.Link line 356
  30. def OAI.CPTSeparation.Reachability.Reach line 358
  31. theorem OAI.CPTSeparation.Reachability.mono line 362
  32. theorem OAI.CPTSeparation.Reachability.left_extend line 367
  33. theorem OAI.CPTSeparation.Reachability.link_eqv line 376
  34. theorem OAI.CPTSeparation.Reachability.reach_eqv line 382
  35. def OAI.CPTSeparation.Reachability.graph line 390
  36. theorem OAI.CPTSeparation.Reachability.eqv_walk line 395
  37. theorem OAI.CPTSeparation.Reachability.walk_reach line 408
  38. theorem OAI.CPTSeparation.Reachability.eqv_iff_bounded line 413
  39. def OAI.CPTSeparation.Counting.PairReach line 431
  40. theorem OAI.CPTSeparation.Counting.uniform_pairReach line 436
  41. theorem OAI.CPTSeparation.Counting.pairReach_lift line 471
  42. theorem OAI.CPTSeparation.Counting.pairReach_eqv line 502
  43. def OAI.CPTSeparation.Interpretations.EncodedDomain line 524
  44. def OAI.CPTSeparation.Interpretations.EncodedLink line 527
  45. def OAI.CPTSeparation.Interpretations.EncodedClass line 531
  46. theorem OAI.CPTSeparation.Interpretations.uniform_domain line 545
  47. theorem OAI.CPTSeparation.Interpretations.uniform_link line 572
  48. theorem OAI.CPTSeparation.Interpretations.uniform_class line 625
  49. def OAI.CPTSeparation.Interpretations.EncodedPayload line 671
  50. def OAI.CPTSeparation.Interpretations.EncodedRep line 675
  51. theorem OAI.CPTSeparation.Interpretations.uniform_payload line 695
  52. theorem OAI.CPTSeparation.Interpretations.uniform_rep line 768
  53. def OAI.CPTSeparation.Interpretations.EncodedUniverse line 793
  54. theorem OAI.CPTSeparation.Interpretations.uniform_universe line 796
  55. def OAI.CPTSeparation.Interpretations.EncodedStateRelation line 808
  56. theorem OAI.CPTSeparation.Interpretations.uniform_stateRelation line 818
  57. structure OAI.CPTSeparation.Interpretations.StateDefinable line 865
  58. theorem OAI.CPTSeparation.Interpretations.StateDefinable.translate line 870
  59. def OAI.CPTSeparation.Interpretations.nextCode line 893
  60. theorem OAI.CPTSeparation.Interpretations.nextCode_injective line 897
  61. theorem OAI.CPTSeparation.Interpretations.StateDefinable.apply line 904
  62. theorem OAI.CPTSeparation.Interpretations.Program.exists_width line 945
  63. theorem OAI.CPTSeparation.Interpretations.Program.family_mono_le line 966
  64. theorem OAI.CPTSeparation.Interpretations.Program.code_mem_domain line 975
  65. def OAI.CPTSeparation.Interpretations.Program.stateCode line 979
  66. theorem OAI.CPTSeparation.Interpretations.Program.stateCode_injective line 982
  67. def OAI.CPTSeparation.Interpretations.Program.inputCode line 987
  68. theorem OAI.CPTSeparation.Interpretations.Program.inputCode_injective line 990
  69. theorem OAI.CPTSeparation.Interpretations.Program.state_definable line 1018
  70. theorem OAI.CPTSeparation.Interpretations.StateDefinable.sentence line 1062
  71. theorem OAI.CPTSeparation.Interpretations.Program.haltsAt_unique line 1079
  72. theorem OAI.CPTSeparation.Interpretations.Program.accepts_iff_of_haltsAt line 1085
  73. theorem OAI.CPTSeparation.Interpretations.Program.synchronize line 1092