OAI/ModelTheory/Choiceless/Operational.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CPTSeparation.Operational.truth_ne_empty line 15
  2. theorem OAI.CPTSeparation.Operational.boolean_truth line 18
  3. lemma OAI.CPTSeparation.Operational.uniqueHF_spec line 21
  4. inductive OAI.CPTSeparation.Operational.Term line 28
  5. abbrev OAI.CPTSeparation.Operational.Valuation line 47
  6. theorem OAI.CPTSeparation.Operational.State.mem_support line 51
  7. def OAI.CPTSeparation.Operational.Term.eval line 60
  8. inductive OAI.CPTSeparation.Operational.Rule line 84
  9. def OAI.CPTSeparation.Operational.Rule.updates line 97
  10. lemma OAI.CPTSeparation.Operational.State.updatedValue_eq line 111
  11. lemma OAI.CPTSeparation.Operational.State.updatedValue_default line 118
  12. instance OAI.CPTSeparation.Operational.(instance at line 124) line 124
  13. structure OAI.CPTSeparation.Operational.Machine line 128
  14. abbrev OAI.CPTSeparation.Operational.Machine.functionArity line 138
  15. abbrev OAI.CPTSeparation.Operational.Machine.Store line 140
  16. def OAI.CPTSeparation.Operational.Machine.flag line 142
  17. def OAI.CPTSeparation.Operational.Machine.step line 144
  18. def OAI.CPTSeparation.Operational.Machine.run line 149
  19. def OAI.CPTSeparation.Operational.Machine.accepts line 153
  20. lemma OAI.CPTSeparation.Hereditary.mem_closure_self line 168
  21. lemma OAI.CPTSeparation.Hereditary.closure_member_subset line 170
  22. lemma OAI.CPTSeparation.Hereditary.mem_closure_iff line 176
  23. lemma OAI.CPTSeparation.Hereditary.closure_transitive line 192
  24. lemma OAI.CPTSeparation.Hereditary.mem_mapEquiv line 197
  25. lemma OAI.CPTSeparation.Hereditary.rtc_map line 207
  26. lemma OAI.CPTSeparation.Hereditary.closure_map line 214
  27. lemma OAI.CPTSeparation.Hereditary.mem_familyClosure line 231
  28. lemma OAI.CPTSeparation.Hereditary.familyClosure_contains line 234
  29. lemma OAI.CPTSeparation.Hereditary.familyClosure_transitive line 237
  30. lemma OAI.CPTSeparation.Operational.State.value_mem_critical line 256
  31. lemma OAI.CPTSeparation.Operational.State.argument_mem_critical line 260
  32. lemma OAI.CPTSeparation.Operational.State.active_transitive line 264
  33. def OAI.CPTSeparation.Operational.Machine.runActive line 274
  34. lemma OAI.CPTSeparation.Operational.Machine.state_active_subset line 279
  35. lemma OAI.CPTSeparation.Operational.Machine.runActive_transitive line 284
  36. lemma OAI.CPTSeparation.Operational.Machine.runActive_card_le line 293
  37. def OAI.CPTSeparation.Operational.Machine.PolynomiallyBounded line 308
  38. abbrev OAI.CPTSeparation.Operational.lift line 323
  39. lemma OAI.CPTSeparation.Operational.lift_empty line 325
  40. lemma OAI.CPTSeparation.Operational.lift_truth line 327
  41. lemma OAI.CPTSeparation.Operational.lift_ordinal line 329
  42. lemma OAI.CPTSeparation.Operational.lift_double line 331
  43. lemma OAI.CPTSeparation.Operational.lift_isSet line 333
  44. lemma OAI.CPTSeparation.Operational.lift_boolean line 335
  45. lemma OAI.CPTSeparation.Operational.lift_truth_iff line 338
  46. lemma OAI.CPTSeparation.Operational.lift_empty_iff line 341
  47. lemma OAI.CPTSeparation.Operational.lift_mem_iff line 344
  48. lemma OAI.CPTSeparation.Operational.lift_elements line 346
  49. lemma OAI.CPTSeparation.Operational.lift_ofFinset line 348
  50. lemma OAI.CPTSeparation.Operational.lift_allAtoms line 350
  51. lemma OAI.CPTSeparation.Operational.lift_union line 361
  52. lemma OAI.CPTSeparation.Operational.lift_unique line 375
  53. lemma OAI.CPTSeparation.Operational.lift_card line 390
  54. lemma OAI.CPTSeparation.Operational.lift_input line 393
  55. def OAI.CPTSeparation.Operational.locationEquiv line 407
  56. lemma OAI.CPTSeparation.Operational.locationEquiv_apply line 410
  57. lemma OAI.CPTSeparation.Operational.locationEquiv_symm_apply line 413
  58. def OAI.CPTSeparation.Operational.State.transport line 418
  59. lemma OAI.CPTSeparation.Operational.State.transport_value line 425
  60. lemma OAI.CPTSeparation.Operational.State.ext_value line 429
  61. lemma OAI.CPTSeparation.Operational.State.transport_initial line 435
  62. lemma OAI.CPTSeparation.Operational.Term.eval_transport line 446
  63. abbrev OAI.CPTSeparation.Operational.updateEquiv line 492
  64. lemma OAI.CPTSeparation.Operational.mem_update_image line 495
  65. lemma OAI.CPTSeparation.Operational.Rule.updates_transport line 505
  66. lemma OAI.CPTSeparation.Operational.State.consistent_transport line 541
  67. lemma OAI.CPTSeparation.Operational.State.applyUpdates_transport line 554
  68. lemma OAI.CPTSeparation.Operational.State.support_transport line 573
  69. lemma OAI.CPTSeparation.Operational.State.critical_transport line 579
  70. lemma OAI.CPTSeparation.Operational.State.active_transport line 588
  71. lemma OAI.CPTSeparation.Operational.Machine.flag_transport line 619
  72. lemma OAI.CPTSeparation.Operational.Machine.step_transport line 636
  73. lemma OAI.CPTSeparation.Operational.Machine.run_transport line 653
  74. lemma OAI.CPTSeparation.Operational.Machine.runActive_transport line 664
  75. lemma OAI.CPTSeparation.Hereditary.closure_ofFinset line 688
  76. lemma OAI.CPTSeparation.Hereditary.closure_subset_of_transitive line 695
  77. lemma OAI.CPTSeparation.Hereditary.elements_subset_closure line 704
  78. lemma OAI.CPTSeparation.Hereditary.closure_atom line 708
  79. lemma OAI.CPTSeparation.Hereditary.closure_double_subset line 712
  80. lemma OAI.CPTSeparation.Hereditary.closure_ordinal line 725
  81. lemma OAI.CPTSeparation.Hereditary.card_closure_ordinal line 743
  82. lemma OAI.CPTSeparation.Operational.closure_union_subset line 756
  83. lemma OAI.CPTSeparation.Operational.closure_unique_subset line 764
  84. lemma OAI.CPTSeparation.Operational.card_closure_card line 771
  85. lemma OAI.CPTSeparation.Operational.card_closure_boolean line 775
  86. lemma OAI.CPTSeparation.Operational.State.empty_mem_active line 782
  87. lemma OAI.CPTSeparation.Operational.State.atoms_mem_active line 786
  88. lemma OAI.CPTSeparation.Operational.State.closure_value_subset_active line 790
  89. lemma OAI.CPTSeparation.Operational.State.closure_atoms_subset_active line 798
  90. def OAI.CPTSeparation.Operational.Term.trace line 807
  91. lemma OAI.CPTSeparation.Operational.Term.closure_eval_subset_trace line 832
  92. def OAI.CPTSeparation.Operational.Term.bound line 864
  93. def OAI.CPTSeparation.Operational.Term.potential line 883
  94. lemma OAI.CPTSeparation.Operational.Term.potential_var line 886
  95. lemma OAI.CPTSeparation.Operational.Term.potential_active line 892
  96. lemma OAI.CPTSeparation.Operational.Term.potential_cons line 895
  97. lemma OAI.CPTSeparation.Operational.Term.card_trace_le line 900