OAI/Computability/WitnessedChoice/Machines.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WitnessedSeparation.Grid.atomSizeConstant_pos line 12
  2. theorem OAI.WitnessedSeparation.Grid.exists_numeric_box line 16
  3. def OAI.WitnessedSeparation.structureQuery line 62
  4. theorem OAI.WitnessedSeparation.Grid.program_agrees_on_some_box line 71
  5. theorem OAI.WitnessedSeparation.query_not_interpretation_definable line 123
  6. abbrev OAI.WitnessedSeparation.Operational.empty line 145
  7. abbrev OAI.WitnessedSeparation.Operational.truth line 147
  8. def OAI.WitnessedSeparation.Operational.boolean line 149
  9. theorem OAI.WitnessedSeparation.Operational.truth_ne_empty line 151
  10. theorem OAI.WitnessedSeparation.Operational.boolean_truth line 154
  11. def OAI.WitnessedSeparation.Operational.inputRelation line 157
  12. def OAI.WitnessedSeparation.Operational.allAtoms line 160
  13. def OAI.WitnessedSeparation.Operational.unionHF line 162
  14. def OAI.WitnessedSeparation.Operational.uniqueHF line 164
  15. lemma OAI.WitnessedSeparation.Operational.uniqueHF_spec line 167
  16. def OAI.WitnessedSeparation.Operational.cardinalityHF line 174
  17. inductive OAI.WitnessedSeparation.Operational.Term line 176
  18. abbrev OAI.WitnessedSeparation.Operational.Location line 195
  19. abbrev OAI.WitnessedSeparation.Operational.Valuation line 197
  20. structure OAI.WitnessedSeparation.Operational.State line 199
  21. def OAI.WitnessedSeparation.Operational.State.initial line 205
  22. def OAI.WitnessedSeparation.Operational.State.support line 207
  23. theorem OAI.WitnessedSeparation.Operational.State.mem_support line 209
  24. def OAI.WitnessedSeparation.Operational.Term.eval line 218
  25. inductive OAI.WitnessedSeparation.Operational.Rule line 242
  26. abbrev OAI.WitnessedSeparation.Operational.Update line 251
  27. def OAI.WitnessedSeparation.Operational.Rule.updates line 257
  28. def OAI.WitnessedSeparation.Operational.State.Consistent line 271
  29. def OAI.WitnessedSeparation.Operational.State.updatedValue line 274
  30. lemma OAI.WitnessedSeparation.Operational.State.updatedValue_eq line 278
  31. lemma OAI.WitnessedSeparation.Operational.State.updatedValue_default line 285
  32. def OAI.WitnessedSeparation.Operational.State.applyUpdates line 289
  33. inductive OAI.WitnessedSeparation.Operational.Control line 301
  34. instance OAI.WitnessedSeparation.Operational.(instance at line 303) line 303
  35. structure OAI.WitnessedSeparation.Operational.Machine line 307
  36. abbrev OAI.WitnessedSeparation.Operational.Machine.functionArity line 317
  37. abbrev OAI.WitnessedSeparation.Operational.Machine.Store line 319
  38. def OAI.WitnessedSeparation.Operational.Machine.flag line 321
  39. def OAI.WitnessedSeparation.Operational.Machine.step line 323
  40. def OAI.WitnessedSeparation.Operational.Machine.run line 328
  41. def OAI.WitnessedSeparation.Operational.Machine.accepts line 332
  42. lemma OAI.WitnessedSeparation.Hereditary.mem_mapEquiv line 353
  43. lemma OAI.WitnessedSeparation.Hereditary.rtc_map line 363
  44. lemma OAI.WitnessedSeparation.Hereditary.closure_map line 370
  45. def OAI.WitnessedSeparation.Hereditary.familyClosure line 387
  46. lemma OAI.WitnessedSeparation.Hereditary.mem_familyClosure line 389
  47. lemma OAI.WitnessedSeparation.Hereditary.familyClosure_contains line 392
  48. lemma OAI.WitnessedSeparation.Hereditary.familyClosure_transitive line 395
  49. def OAI.WitnessedSeparation.Operational.State.critical line 418
  50. lemma OAI.WitnessedSeparation.Operational.State.value_mem_critical line 421
  51. lemma OAI.WitnessedSeparation.Operational.State.argument_mem_critical line 425
  52. def OAI.WitnessedSeparation.Operational.State.active line 429
  53. lemma OAI.WitnessedSeparation.Operational.State.active_transitive line 432
  54. def OAI.WitnessedSeparation.Operational.Machine.runActive line 442
  55. lemma OAI.WitnessedSeparation.Operational.Machine.state_active_subset line 447
  56. lemma OAI.WitnessedSeparation.Operational.Machine.runActive_transitive line 452
  57. lemma OAI.WitnessedSeparation.Operational.Machine.runActive_card_le line 461
  58. def OAI.WitnessedSeparation.Operational.Machine.PolynomiallyBounded line 476
  59. abbrev OAI.WitnessedSeparation.Operational.lift line 497
  60. lemma OAI.WitnessedSeparation.Operational.lift_empty line 499
  61. lemma OAI.WitnessedSeparation.Operational.lift_truth line 501
  62. lemma OAI.WitnessedSeparation.Operational.lift_ordinal line 503
  63. lemma OAI.WitnessedSeparation.Operational.lift_double line 505
  64. lemma OAI.WitnessedSeparation.Operational.lift_isSet line 507
  65. lemma OAI.WitnessedSeparation.Operational.lift_boolean line 509
  66. lemma OAI.WitnessedSeparation.Operational.lift_truth_iff line 512
  67. lemma OAI.WitnessedSeparation.Operational.lift_empty_iff line 515
  68. lemma OAI.WitnessedSeparation.Operational.lift_mem_iff line 518
  69. lemma OAI.WitnessedSeparation.Operational.lift_elements line 520
  70. lemma OAI.WitnessedSeparation.Operational.lift_ofFinset line 522
  71. lemma OAI.WitnessedSeparation.Operational.lift_allAtoms line 524
  72. lemma OAI.WitnessedSeparation.Operational.lift_union line 535
  73. lemma OAI.WitnessedSeparation.Operational.lift_unique line 549
  74. lemma OAI.WitnessedSeparation.Operational.lift_card line 564
  75. lemma OAI.WitnessedSeparation.Operational.lift_input line 567
  76. def OAI.WitnessedSeparation.Operational.locationEquiv line 581
  77. lemma OAI.WitnessedSeparation.Operational.locationEquiv_apply line 584
  78. lemma OAI.WitnessedSeparation.Operational.locationEquiv_symm_apply line 587
  79. def OAI.WitnessedSeparation.Operational.State.transport line 592
  80. lemma OAI.WitnessedSeparation.Operational.State.transport_value line 599
  81. lemma OAI.WitnessedSeparation.Operational.State.ext_value line 603
  82. lemma OAI.WitnessedSeparation.Operational.State.transport_initial line 609
  83. lemma OAI.WitnessedSeparation.Operational.Term.eval_transport line 620
  84. abbrev OAI.WitnessedSeparation.Operational.updateEquiv line 666
  85. lemma OAI.WitnessedSeparation.Operational.mem_update_image line 669
  86. lemma OAI.WitnessedSeparation.Operational.Rule.updates_transport line 679
  87. lemma OAI.WitnessedSeparation.Operational.State.consistent_transport line 715
  88. lemma OAI.WitnessedSeparation.Operational.State.applyUpdates_transport line 728
  89. lemma OAI.WitnessedSeparation.Operational.State.support_transport line 747
  90. lemma OAI.WitnessedSeparation.Operational.State.critical_transport line 753
  91. lemma OAI.WitnessedSeparation.Operational.State.active_transport line 762
  92. lemma OAI.WitnessedSeparation.Operational.Machine.flag_transport line 793
  93. lemma OAI.WitnessedSeparation.Operational.Machine.step_transport line 804
  94. lemma OAI.WitnessedSeparation.Operational.Machine.run_transport line 821
  95. lemma OAI.WitnessedSeparation.Operational.Machine.runActive_transport line 832
  96. lemma OAI.WitnessedSeparation.Hereditary.closure_ofFinset line 862
  97. lemma OAI.WitnessedSeparation.Hereditary.closure_subset_of_transitive line 869
  98. lemma OAI.WitnessedSeparation.Hereditary.elements_subset_closure line 878
  99. lemma OAI.WitnessedSeparation.Hereditary.closure_atom line 882
  100. lemma OAI.WitnessedSeparation.Hereditary.closure_double_subset line 886
  101. lemma OAI.WitnessedSeparation.Hereditary.closure_ordinal line 899
  102. lemma OAI.WitnessedSeparation.Hereditary.card_closure_ordinal line 917