OAI/Computability/WitnessedChoice/Syntax.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WitnessedChoice.stateCode_inj line 15
  2. theorem OAI.WitnessedChoice.smul_stateCode line 20
  3. theorem OAI.WitnessedChoice.smul_choiceCode line 28
  4. theorem OAI.WitnessedChoice.stateCode_fixed_of_pointwise line 32
  5. theorem OAI.WitnessedChoice.Selection.choices_nonempty line 43
  6. theorem OAI.WitnessedChoice.Selection.some_mem_choices line 49
  7. theorem OAI.WitnessedChoice.Selection.none_mem_choices line 58
  8. theorem OAI.WitnessedChoice.Selection.advance_mono line 63
  9. theorem OAI.WitnessedChoice.Selection.advance_card line 68
  10. theorem OAI.WitnessedChoice.Selection.Prefix.restrict line 78
  11. theorem OAI.WitnessedChoice.Selection.Prefix.monotone line 82
  12. theorem OAI.WitnessedChoice.Selection.Prefix.card_eq line 92
  13. theorem OAI.WitnessedChoice.Selection.FirstStabilization.length_le line 102
  14. theorem OAI.WitnessedChoice.Selection.exists_first_stabilization line 108
  15. theorem OAI.WitnessedChoice.Selection.Filtered.history line 122
  16. theorem OAI.WitnessedChoice.Selection.Filtered.witnessed line 131
  17. theorem OAI.WitnessedChoice.Selection.Filtered.all_paths_witnessed line 148
  18. theorem OAI.WitnessedChoice.choiceCode_inj line 172
  19. theorem OAI.WitnessedChoice.image_mul line 195
  20. theorem OAI.WitnessedChoice.image_inv_image line 200
  21. theorem OAI.WitnessedChoice.Selection.Equivariant.transitiveAt line 210
  22. theorem OAI.WitnessedChoice.Selection.Equivariant.transitiveAt_iff line 223
  23. theorem OAI.WitnessedChoice.Selection.Equivariant.choices_image line 233
  24. theorem OAI.WitnessedChoice.Selection.advance_image line 245
  25. theorem OAI.WitnessedChoice.Selection.match_prefixes line 249
  26. theorem OAI.WitnessedChoice.Selection.first_stabilization_unique_length line 286
  27. theorem OAI.WitnessedChoice.Selection.terminal_orbit line 301
  28. def OAI.WitnessedChoice.Selection.selected line 310
  29. theorem OAI.WitnessedChoice.Selection.selected_mem line 313
  30. def OAI.WitnessedChoice.Selection.run line 316
  31. theorem OAI.WitnessedChoice.Selection.run_prefix line 321
  32. theorem OAI.WitnessedChoice.Selection.exists_path line 324
  33. def OAI.WitnessedChoice.BGS.decodeState line 346
  34. def OAI.WitnessedChoice.BGS.decodeChoice line 348
  35. theorem OAI.WitnessedChoice.BGS.decodeState_code line 351
  36. theorem OAI.WitnessedChoice.BGS.decodeChoice_code line 355
  37. theorem OAI.WitnessedChoice.BGS.TC_stateCode line 370
  38. structure OAI.WitnessedChoice.BGS.Realizes line 378
  39. theorem OAI.WitnessedChoice.BGS.Realizes.prefix_decode line 397
  40. theorem OAI.WitnessedChoice.BGS.Realizes.first_decode line 440
  41. theorem OAI.WitnessedChoice.BGS.Realizes.good line 449
  42. theorem OAI.WitnessedChoice.BGS.Realizes.boolean line 513
  43. def OAI.WitnessedChoice.BGS.liftRen line 537
  44. lemma OAI.WitnessedChoice.BGS.liftRen_zero line 540
  45. lemma OAI.WitnessedChoice.BGS.liftRen_succ line 542
  46. lemma OAI.WitnessedChoice.BGS.cons_comp_liftRen line 545
  47. def OAI.Term.up line 652
  48. def OAI.Formula.up line 654
  49. def OAI.Formula.truth line 656
  50. def OAI.Formula.falsity line 658
  51. def OAI.Term.singleton line 660
  52. def OAI.Term.cup line 662
  53. def OAI.Term.orderedPair line 664
  54. def OAI.Formula.existsIn line 666
  55. def OAI.Formula.allIn line 669
  56. def OAI.Formula.mem line 672
  57. def OAI.Formula.imp line 675
  58. def OAI.Formula.iff line 677
  59. def OAI.Term.inter line 679
  60. def OAI.Term.diff line 682
  61. def OAI.Term.when line 685
  62. def OAI.Term.cond line 688
  63. def OAI.Term.product line 691
  64. theorem OAI.Term.up_count line 694
  65. theorem OAI.Formula.up_count line 697
  66. theorem OAI.Term.eval_up line 700
  67. theorem OAI.Formula.eval_up line 705
  68. lemma OAI.collect_pure line 711
  69. lemma OAI.elements_emptyHF line 717
  70. lemma OAI.uniqueHF_singleton line 720
  71. lemma OAI.uniqueHF_empty line 727
  72. lemma OAI.unionHF_double line 733
  73. lemma OAI.Formula.eval_truth line 737
  74. lemma OAI.Formula.eval_existsIn line 741
  75. lemma OAI.Formula.eval_allIn line 757
  76. lemma OAI.Term.eval_singleton line 772
  77. lemma OAI.Term.eval_cup line 778
  78. lemma OAI.Term.eval_orderedPair line 784
  79. lemma OAI.Formula.eval_mem line 791
  80. lemma OAI.Term.eval_when line 803
  81. lemma OAI.Term.eval_cond line 818
  82. def OAI.Term.letIn line 834
  83. def OAI.Formula.letIn line 837
  84. lemma OAI.Term.eval_letIn line 840
  85. lemma OAI.Formula.eval_letIn line 850
  86. lemma WitnessedChoice.BGS.cons_two line 876
  87. def WitnessedChoice.BGS.Term.mapSet line 881
  88. def WitnessedChoice.BGS.Term.bindSet line 884
  89. def WitnessedChoice.BGS.Term.addPairBody line 887
  90. def WitnessedChoice.BGS.Term.partialPool line 890
  91. def WitnessedChoice.BGS.Term.completeRelation line 895
  92. def WitnessedChoice.BGS.Term.identityRelation line 899
  93. def WitnessedChoice.BGS.Term.localPool line 902
  94. lemma WitnessedChoice.BGS.Term.mapSet_count line 905
  95. lemma WitnessedChoice.BGS.Term.bindSet_count line 909
  96. lemma WitnessedChoice.BGS.Term.partialPool_count line 912
  97. lemma WitnessedChoice.BGS.Term.completeRelation_count line 919
  98. lemma WitnessedChoice.BGS.Term.identityRelation_count line 921
  99. lemma WitnessedChoice.BGS.Term.localPool_count line 923
  100. lemma WitnessedChoice.BGS.Term.eval_comprehend line 929
  101. lemma WitnessedChoice.BGS.Term.eval_mapSet line 941
  102. lemma WitnessedChoice.BGS.Term.eval_bindSet line 951
  103. lemma WitnessedChoice.BGS.Term.eval_addPairBody line 963