OAI/Computability/WitnessedChoice/EncodedCounting.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WitnessedSeparation.Interpretations.EncodedDomain line 20
  2. def OAI.WitnessedSeparation.Interpretations.EncodedLink line 23
  3. def OAI.WitnessedSeparation.Interpretations.EncodedClass line 27
  4. theorem OAI.WitnessedSeparation.Interpretations.uniform_domain line 41
  5. theorem OAI.WitnessedSeparation.Interpretations.uniform_link line 68
  6. theorem OAI.WitnessedSeparation.Interpretations.uniform_class line 121
  7. def OAI.WitnessedSeparation.Interpretations.EncodedPayload line 171
  8. def OAI.WitnessedSeparation.Interpretations.EncodedRep line 175
  9. theorem OAI.WitnessedSeparation.Interpretations.uniform_payload line 195
  10. theorem OAI.WitnessedSeparation.Interpretations.uniform_rep line 272
  11. def OAI.WitnessedSeparation.Interpretations.EncodedUniverse line 297
  12. theorem OAI.WitnessedSeparation.Interpretations.uniform_universe line 300
  13. def OAI.WitnessedSeparation.Interpretations.EncodedStateRelation line 312
  14. theorem OAI.WitnessedSeparation.Interpretations.uniform_stateRelation line 322
  15. structure OAI.WitnessedSeparation.Interpretations.StateDefinable line 375
  16. theorem OAI.WitnessedSeparation.Interpretations.StateDefinable.translate line 380
  17. def OAI.WitnessedSeparation.Interpretations.nextCode line 403
  18. theorem OAI.WitnessedSeparation.Interpretations.nextCode_injective line 407
  19. theorem OAI.WitnessedSeparation.Interpretations.StateDefinable.apply line 414
  20. theorem OAI.WitnessedSeparation.Interpretations.Program.exists_width line 461
  21. theorem OAI.WitnessedSeparation.Interpretations.Program.family_mono_le line 482
  22. theorem OAI.WitnessedSeparation.Interpretations.Program.code_mem_domain line 491
  23. def OAI.WitnessedSeparation.Interpretations.Program.stateCode line 495
  24. theorem OAI.WitnessedSeparation.Interpretations.Program.stateCode_injective line 498
  25. def OAI.WitnessedSeparation.Interpretations.Program.inputCode line 503
  26. theorem OAI.WitnessedSeparation.Interpretations.Program.inputCode_injective line 506
  27. theorem OAI.WitnessedSeparation.Interpretations.Program.state_definable line 534
  28. theorem OAI.WitnessedSeparation.Interpretations.StateDefinable.sentence line 584
  29. theorem OAI.WitnessedSeparation.Interpretations.Program.haltsAt_unique line 601
  30. theorem OAI.WitnessedSeparation.Interpretations.Program.accepts_iff_of_haltsAt line 607
  31. theorem OAI.WitnessedSeparation.Interpretations.Program.synchronize line 614
  32. theorem OAI.WitnessedSeparation.Grid.four_fibers line 647
  33. theorem OAI.WitnessedSeparation.Grid.edgeFaces_card_le line 672
  34. def OAI.WitnessedSeparation.Grid.localSizeBound line 720
  35. theorem OAI.WitnessedSeparation.Grid.localGroup_card_le line 722
  36. theorem OAI.WitnessedSeparation.Grid.configuration_card_le line 733
  37. def OAI.WitnessedSeparation.Grid.atomSizeConstant line 745
  38. theorem OAI.WitnessedSeparation.Grid.atom_card_bounds line 747
  39. theorem OAI.WitnessedSeparation.Hereditary.hereditary_iff line 788
  40. theorem OAI.WitnessedSeparation.Hereditary.hereditary_transitive line 798
  41. theorem OAI.WitnessedSeparation.Hereditary.ordinal_hereditary line 801
  42. abbrev OAI.WitnessedSeparation.Grid.programInput line 828
  43. def OAI.WitnessedSeparation.Grid.programActionIso line 833
  44. theorem OAI.WitnessedSeparation.Grid.trace_supported line 839
  45. def OAI.WitnessedSeparation.Grid.programDomain line 855
  46. def OAI.WitnessedSeparation.Grid.programHF line 857
  47. theorem OAI.WitnessedSeparation.Grid.program_domain_transitive line 860
  48. theorem OAI.WitnessedSeparation.Grid.program_mem_uniform line 864
  49. theorem OAI.WitnessedSeparation.Grid.program_set_uniform line 868
  50. theorem OAI.WitnessedSeparation.Grid.program_pure line 875
  51. theorem OAI.WitnessedSeparation.Grid.program_input_definable line 883
  52. def OAI.WitnessedSeparation.Grid.twoCharges line 923
  53. theorem OAI.WitnessedSeparation.Grid.stage_sentence_agrees line 947
  54. lemma OAI.WitnessedSeparation.Quantitative.const_little_rpow line 989
  55. lemma OAI.WitnessedSeparation.Quantitative.power_little_power line 993
  56. lemma OAI.WitnessedSeparation.Quantitative.ceil_little line 1002
  57. def OAI.WitnessedSeparation.Quantitative.radius line 1015
  58. def OAI.WitnessedSeparation.Quantitative.palette line 1017
  59. lemma OAI.WitnessedSeparation.Quantitative.log_volume_little line 1019
  60. lemma OAI.WitnessedSeparation.Quantitative.radius_little line 1029
  61. lemma OAI.WitnessedSeparation.Quantitative.radius_little_palette line 1045
  62. lemma OAI.WitnessedSeparation.Quantitative.homogeneity_little line 1049
  63. lemma OAI.WitnessedSeparation.Quantitative.floor_big line 1068
  64. lemma OAI.WitnessedSeparation.Quantitative.giant_little line 1074
  65. theorem OAI.WitnessedSeparation.Quantitative.eventual_bounds line 1089
  66. def OAI.WitnessedSeparation.Quantitative.timeExponent line 1120
  67. def OAI.WitnessedSeparation.Quantitative.traceExponent line 1122
  68. lemma OAI.WitnessedSeparation.Quantitative.timeExponent_ge_two line 1124
  69. lemma OAI.WitnessedSeparation.Quantitative.nat_le_power line 1126
  70. lemma OAI.WitnessedSeparation.Quantitative.polynomial_bounds line 1134
  71. lemma OAI.WitnessedSeparation.Quantitative.real_trace_bound line 1160
  72. lemma OAI.WitnessedSeparation.Interpretations.Program.stage_le_cost line 1177
  73. lemma OAI.WitnessedSeparation.Interpretations.Program.size_le_cost line 1181