OAI/Computability/WitnessedChoice/CountingTransfer.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WitnessedSeparation.HFCoding.Domain line 14
  2. def OAI.WitnessedSeparation.HFCoding.SingletonTest line 20
  3. def OAI.WitnessedSeparation.HFCoding.DoubleTest line 23
  4. theorem OAI.WitnessedSeparation.HFCoding.singletonTest_iff line 28
  5. theorem OAI.WitnessedSeparation.HFCoding.doubleTest_iff line 47
  6. def OAI.WitnessedSeparation.HFCoding.PairTest line 69
  7. theorem OAI.WitnessedSeparation.HFCoding.pairTest_iff line 72
  8. theorem OAI.WitnessedSeparation.HFCoding.singleton_definable line 95
  9. theorem OAI.WitnessedSeparation.HFCoding.double_definable line 105
  10. theorem OAI.WitnessedSeparation.HFCoding.pair_definable line 114
  11. theorem OAI.WitnessedSeparation.HFCoding.ordinal_definable line 126
  12. def OAI.WitnessedSeparation.Counting.UniformDefinable line 170
  13. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.congr line 178
  14. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.reindex line 184
  15. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.falsum line 193
  16. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.neg line 196
  17. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.and line 201
  18. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.or line 208
  19. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.imp line 212
  20. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.iff line 216
  21. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.equal line 220
  22. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.relation line 226
  23. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.fresh line 233
  24. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.updated_args line 243
  25. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.free_binder line 251
  26. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.ex line 261
  27. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.all line 272
  28. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.exact line 276
  29. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.exists_finset line 287
  30. theorem OAI.WitnessedSeparation.Counting.UniformDefinable.bounded_hartig line 295
  31. theorem OAI.WitnessedSeparation.HFCoding.uniform_singleton line 330
  32. theorem OAI.WitnessedSeparation.HFCoding.uniform_double line 339
  33. theorem OAI.WitnessedSeparation.HFCoding.uniform_pair line 352
  34. theorem OAI.WitnessedSeparation.HFCoding.uniform_ordinal line 364
  35. structure OAI.WitnessedSeparation.Interpretations.Structure.Iso line 408
  36. def OAI.WitnessedSeparation.Interpretations.Structure.Iso.symm line 416
  37. theorem OAI.WitnessedSeparation.Interpretations.Structure.Iso.eval line 420
  38. def OAI.WitnessedSeparation.Interpretations.Interpretation.domainEquiv line 450
  39. theorem OAI.WitnessedSeparation.Interpretations.Interpretation.domainEquiv_val line 457
  40. theorem OAI.WitnessedSeparation.Interpretations.Interpretation.link_equiv line 460
  41. theorem OAI.WitnessedSeparation.Interpretations.Interpretation.eqvGen_map line 467
  42. theorem OAI.WitnessedSeparation.Interpretations.Interpretation.class_equiv line 477
  43. def OAI.WitnessedSeparation.Interpretations.Interpretation.vertexEquiv line 488
  44. theorem OAI.WitnessedSeparation.Interpretations.Interpretation.vertexEquiv_mk line 490
  45. def OAI.WitnessedSeparation.Interpretations.Interpretation.applyIso line 493
  46. theorem OAI.WitnessedSeparation.Interpretations.map_payload line 537
  47. theorem OAI.WitnessedSeparation.Interpretations.map_vertexCode line 554
  48. theorem OAI.WitnessedSeparation.Interpretations.map_mem_wrappers line 559
  49. theorem OAI.WitnessedSeparation.Interpretations.map_mem_pairFamily line 564
  50. theorem OAI.WitnessedSeparation.Interpretations.map_mem_classFamily line 572
  51. def OAI.WitnessedSeparation.Interpretations.Program.stateIso line 588
  52. def OAI.WitnessedSeparation.Interpretations.Program.code line 592
  53. theorem OAI.WitnessedSeparation.Interpretations.Program.code_injective line 596
  54. theorem OAI.WitnessedSeparation.Interpretations.Program.map_code line 601
  55. def OAI.WitnessedSeparation.Interpretations.Program.baseFamily line 609
  56. def OAI.WitnessedSeparation.Interpretations.Program.family line 612
  57. theorem OAI.WitnessedSeparation.Interpretations.Program.family_mono line 619
  58. theorem OAI.WitnessedSeparation.Interpretations.Program.base_subset_family line 622
  59. theorem OAI.WitnessedSeparation.Interpretations.Program.atom_mem_family line 627
  60. theorem OAI.WitnessedSeparation.Interpretations.Program.ordinal_mem_family line 630
  61. theorem OAI.WitnessedSeparation.Interpretations.Program.code_mem_family line 633
  62. theorem OAI.WitnessedSeparation.Interpretations.Program.baseFamily_transitive line 642
  63. theorem OAI.WitnessedSeparation.Interpretations.Program.family_transitive line 652
  64. theorem OAI.WitnessedSeparation.Interpretations.Program.map_mem_baseFamily line 666
  65. theorem OAI.WitnessedSeparation.Interpretations.Program.map_mem_family line 674
  66. theorem OAI.WitnessedSeparation.Interpretations.Program.baseFamily_card_le line 697
  67. theorem OAI.WitnessedSeparation.Interpretations.Program.family_card_le line 704
  68. theorem OAI.WitnessedSeparation.Interpretations.Program.trace_family line 734
  69. def OAI.WitnessedSeparation.Interpretations.Formula.scopedWidth line 758
  70. theorem OAI.WitnessedSeparation.Interpretations.Formula.context_le_width line 767
  71. def OAI.WitnessedSeparation.Interpretations.guardedEquiv line 777
  72. theorem OAI.WitnessedSeparation.Interpretations.count_comparison line 789
  73. theorem OAI.WitnessedSeparation.Interpretations.uniform_translate line 825
  74. def OAI.WitnessedSeparation.Reachability.Link line 890
  75. def OAI.WitnessedSeparation.Reachability.Reach line 892
  76. theorem OAI.WitnessedSeparation.Reachability.mono line 896
  77. theorem OAI.WitnessedSeparation.Reachability.left_extend line 901
  78. theorem OAI.WitnessedSeparation.Reachability.link_eqv line 910
  79. theorem OAI.WitnessedSeparation.Reachability.reach_eqv line 916
  80. def OAI.WitnessedSeparation.Reachability.graph line 924
  81. theorem OAI.WitnessedSeparation.Reachability.eqv_walk line 929
  82. theorem OAI.WitnessedSeparation.Reachability.walk_reach line 942
  83. theorem OAI.WitnessedSeparation.Reachability.eqv_iff_bounded line 947
  84. def OAI.WitnessedSeparation.Counting.PairReach line 969
  85. theorem OAI.WitnessedSeparation.Counting.uniform_pairReach line 974
  86. theorem OAI.WitnessedSeparation.Counting.pairReach_lift line 1015
  87. theorem OAI.WitnessedSeparation.Counting.pairReach_eqv line 1037