OAI/Computability/WitnessedChoice/Counting.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WitnessedSeparation.Grid.shiftLocal line 14
  2. theorem OAI.WitnessedSeparation.Grid.shiftLocal_face line 17
  3. theorem OAI.WitnessedSeparation.Grid.shiftLocal_flow line 21
  4. theorem OAI.WitnessedSeparation.Grid.shiftLocal_zero line 25
  5. theorem OAI.WitnessedSeparation.Grid.shiftLocal_add line 28
  6. def OAI.WitnessedSeparation.Grid.localShiftEquiv line 32
  7. def OAI.WitnessedSeparation.Grid.shiftStates line 38
  8. theorem OAI.WitnessedSeparation.Grid.shiftStates_compatible line 41
  9. theorem OAI.WitnessedSeparation.Grid.shiftStates_divergence line 46
  10. def OAI.WitnessedSeparation.Grid.Configuration.shift line 50
  11. theorem OAI.WitnessedSeparation.Grid.Configuration.shift_state line 56
  12. def OAI.WitnessedSeparation.Grid.configShiftEquiv line 60
  13. inductive OAI.WitnessedSeparation.Grid.AtomShift line 67
  14. theorem OAI.WitnessedSeparation.Grid.AtomShift.symm line 73
  15. theorem OAI.WitnessedSeparation.Grid.AtomShift.functional line 82
  16. theorem OAI.WitnessedSeparation.Grid.AtomShift.equal_iff line 86
  17. theorem OAI.WitnessedSeparation.Grid.AtomShift.relation line 92
  18. theorem OAI.WitnessedSeparation.Grid.AtomShift.relation_iff line 106
  19. def OAI.WitnessedSeparation.Grid.blockShiftEquiv line 111
  20. theorem OAI.WitnessedSeparation.Grid.blockShiftEquiv_edge line 116
  21. theorem OAI.WitnessedSeparation.Grid.blockShiftEquiv_config line 120
  22. structure OAI.WitnessedSeparation.Counting.Structure line 136
  23. inductive OAI.WitnessedSeparation.Counting.Formula line 139
  24. def OAI.WitnessedSeparation.Counting.Formula.free line 153
  25. def OAI.WitnessedSeparation.Counting.Formula.eval line 162
  26. theorem OAI.WitnessedSeparation.Counting.Formula.eval_congr line 171
  27. theorem OAI.WitnessedSeparation.Counting.Formula.eval_of_bijectionSystem line 203
  28. def OAI.WitnessedSeparation.Counting.Formula.conjoin line 233
  29. theorem OAI.WitnessedSeparation.Counting.Formula.eval_conjoin line 237
  30. theorem OAI.WitnessedSeparation.Counting.Formula.free_conjoin_subset line 243
  31. def OAI.WitnessedSeparation.Counting.typeOf line 254
  32. theorem OAI.WitnessedSeparation.Counting.typeOf_eq_iff line 257
  33. theorem OAI.WitnessedSeparation.Counting.type_separator line 268
  34. theorem OAI.WitnessedSeparation.Counting.isolate_type line 281
  35. theorem OAI.WitnessedSeparation.Counting.extension_equiv line 329
  36. def OAI.WitnessedSeparation.Counting.Formula.rename line 367
  37. theorem OAI.WitnessedSeparation.Counting.Formula.free_rename line 376
  38. theorem OAI.WitnessedSeparation.Counting.Formula.eval_rename line 387
  39. theorem OAI.WitnessedSeparation.Counting.typeOf_project line 409
  40. theorem OAI.WitnessedSeparation.Counting.typeOf_congr line 417
  41. theorem OAI.WitnessedSeparation.Counting.typeOf_permute line 423
  42. theorem OAI.WitnessedSeparation.Counting.extension_bijection line 438
  43. theorem OAI.WitnessedSeparation.Counting.extend_type line 466
  44. def OAI.WitnessedSeparation.Counting.tupleNames line 499
  45. theorem OAI.WitnessedSeparation.Counting.mem_tupleNames line 502
  46. def OAI.WitnessedSeparation.Counting.tupleAssignment line 505
  47. theorem OAI.WitnessedSeparation.Counting.tupleAssignment_apply line 508
  48. def OAI.WitnessedSeparation.Counting.tupleType line 515
  49. theorem OAI.WitnessedSeparation.Counting.tupleType_assignment line 518
  50. theorem OAI.WitnessedSeparation.Counting.tupleType_project line 526
  51. theorem OAI.WitnessedSeparation.Counting.tupleType_extend line 556
  52. theorem OAI.WitnessedSeparation.Counting.tupleType_append line 609
  53. theorem OAI.WitnessedSeparation.Counting.eval_iso line 626
  54. theorem OAI.WitnessedSeparation.Counting.tupleType_iso line 643
  55. abbrev OAI.WitnessedSeparation.Grid.ClassLabel line 667
  56. instance OAI.WitnessedSeparation.Grid.(instance at line 671) line 671
  57. def OAI.WitnessedSeparation.Grid.classLabel line 676
  58. def OAI.WitnessedSeparation.Grid.classIndex line 680
  59. inductive OAI.WitnessedSeparation.Grid.AnalysisSymbol line 683
  60. def OAI.WitnessedSeparation.Grid.rawDifference line 689
  61. def OAI.WitnessedSeparation.Grid.analysisStructure line 693
  62. theorem OAI.WitnessedSeparation.Grid.classLabel_shiftLocal line 699
  63. theorem OAI.WitnessedSeparation.Grid.classLabel_shiftConfig line 703
  64. theorem OAI.WitnessedSeparation.Grid.AtomShift.classLabel line 708
  65. theorem OAI.WitnessedSeparation.Grid.AtomShift.analysisRelation line 712
  66. def OAI.WitnessedSeparation.Grid.predecessors line 727
  67. theorem OAI.WitnessedSeparation.Grid.predecessors_recovers_class line 729
  68. def OAI.WitnessedSeparation.Grid.classFormula line 748
  69. theorem OAI.WitnessedSeparation.Grid.free_classFormula line 751
  70. theorem OAI.WitnessedSeparation.Grid.eval_classFormula line 758
  71. theorem OAI.WitnessedSeparation.Grid.type_recovers_classes line 775
  72. abbrev OAI.WitnessedSeparation.Grid.Block line 798
  73. def OAI.WitnessedSeparation.Grid.atomBlock line 800
  74. def OAI.WitnessedSeparation.Grid.blockEdges line 804
  75. def OAI.WitnessedSeparation.Grid.touch line 808
  76. theorem OAI.WitnessedSeparation.Grid.blockEdges_card line 810
  77. theorem OAI.WitnessedSeparation.Grid.touch_card line 820
  78. theorem OAI.WitnessedSeparation.Grid.touch_shift line 822
  79. theorem OAI.WitnessedSeparation.Grid.AtomShift.congr line 825
  80. def OAI.WitnessedSeparation.Grid.touches line 844
  81. theorem OAI.WitnessedSeparation.Grid.touches_card line 847
  82. theorem OAI.WitnessedSeparation.Grid.touch_subset_touches line 854
  83. theorem OAI.WitnessedSeparation.Grid.touches_mono line 858
  84. theorem OAI.WitnessedSeparation.Grid.touches_insert_update line 864
  85. def OAI.WitnessedSeparation.Grid.HasState line 890
  86. theorem OAI.WitnessedSeparation.Grid.hasState_edge line 893
  87. theorem OAI.WitnessedSeparation.Grid.hasState_config line 901
  88. def OAI.WitnessedSeparation.Grid.stateAt line 912
  89. theorem OAI.WitnessedSeparation.Grid.stateAt_edge line 923
  90. theorem OAI.WitnessedSeparation.Grid.stateAt_config line 927
  91. theorem OAI.WitnessedSeparation.Grid.hasState_stateAt line 930
  92. theorem OAI.WitnessedSeparation.Grid.classLabel_edge_iff line 942
  93. theorem OAI.WitnessedSeparation.Grid.atomShift_of_states line 958
  94. abbrev OAI.WitnessedSeparation.Grid.Occurrences line 996
  95. def OAI.WitnessedSeparation.Grid.occurrenceAtom line 998
  96. def OAI.WitnessedSeparation.Grid.Augment line 1001
  97. structure OAI.WitnessedSeparation.Grid.SameDiagram line 1004
  98. theorem OAI.WitnessedSeparation.Grid.augmented_diagram_shift line 1010
  99. theorem OAI.WitnessedSeparation.Grid.sameDiagram_of_type line 1065