OAI/GroupTheory/PeriodicGroups/Rules/LocalSyntax.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.SourceBurnside.LocalSyntax.Marker line 10
  2. inductive OAI.SourceBurnside.LocalSyntax.Position line 14
  3. structure OAI.SourceBurnside.LocalSyntax.Metadata line 20
  4. structure OAI.SourceBurnside.LocalSyntax.Skeleton line 26
  5. def OAI.SourceBurnside.LocalSyntax.Skeleton.first line 35
  6. def OAI.SourceBurnside.LocalSyntax.Skeleton.last line 38
  7. def OAI.SourceBurnside.LocalSyntax.Skeleton.Admissible line 41
  8. def OAI.SourceBurnside.LocalSyntax.Skeleton.leftExternal line 44
  9. def OAI.SourceBurnside.LocalSyntax.Skeleton.rightExternal line 47
  10. def OAI.SourceBurnside.LocalSyntax.Skeleton.acceptsLeft line 50
  11. def OAI.SourceBurnside.LocalSyntax.Skeleton.acceptsRight line 53
  12. def OAI.SourceBurnside.LocalSyntax.Skeleton.Structural line 56
  13. def OAI.SourceBurnside.LocalSyntax.Skeleton.Internal line 65
  14. def OAI.SourceBurnside.LocalSyntax.Skeleton.Pair line 70
  15. def OAI.SourceBurnside.LocalSyntax.Skeleton.mark line 76
  16. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.mark_first line 78
  17. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.mark_last line 79
  18. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.mark_pos line 80
  19. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.mark_metadata line 81
  20. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.mark_marker line 83
  21. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.structural_mark_left line 86
  22. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.structural_mark_right line 88
  23. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.internal_mark_left line 90
  24. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.internal_mark_right line 92
  25. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.left_wing_head line 95
  26. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.right_wing_head line 103
  27. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.cursor_left line 109
  28. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.cursor_right line 113
  29. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.create_left line 118
  30. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.finish_right line 123
  31. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.full_move_pair line 128
  32. def OAI.SourceBurnside.LocalSyntax.Skeleton.Link line 138
  33. def OAI.SourceBurnside.LocalSyntax.Skeleton.Closed line 144
  34. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.link_left_wing_head line 148
  35. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.link_right_wing_head line 155
  36. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.link_cursor_right line 161
  37. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.link_create_left line 167
  38. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.link_finish_right line 173
  39. lemma OAI.SourceBurnside.LocalSyntax.chain_change_head line 184
  40. lemma OAI.SourceBurnside.LocalSyntax.chain_change_last line 190
  41. lemma OAI.SourceBurnside.LocalSyntax.chain_replace_one line 201
  42. lemma OAI.SourceBurnside.LocalSyntax.chain_replace_two line 207
  43. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.closed_replace_one line 219
  44. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.closed_replace_two line 232
  45. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.admissible_idle line 247
  46. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.admissible_boundary line 249
  47. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.admissible_full line 251
  48. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.admissible_left line 253
  49. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.admissible_right line 255
  50. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.acquire_conditions line 258
  51. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.full_conditions line 265
  52. inductive OAI.SourceBurnside.LocalSyntax.Skeleton.Replacement line 271
  53. theorem OAI.SourceBurnside.LocalSyntax.Skeleton.replacement_context line 281
  54. def OAI.SourceBurnside.LocalSyntax.Skeleton.Step line 317
  55. abbrev OAI.SourceBurnside.LocalSyntax.Skeleton.Reach line 319
  56. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.closed_step_iff line 321
  57. theorem OAI.SourceBurnside.LocalSyntax.Skeleton.closed_reach line 325
  58. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.external_entrance line 330
  59. def OAI.SourceBurnside.LocalSyntax.Skeleton.InternalPair line 336
  60. def OAI.SourceBurnside.LocalSyntax.Skeleton.IsHead line 338
  61. instance OAI.SourceBurnside.LocalSyntax.Skeleton.(instance at line 340) line 340
  62. def OAI.SourceBurnside.LocalSyntax.Skeleton.RegionForm line 343
  63. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.internal_marker_rule line 348
  64. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.right_wing_constant line 357
  65. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.form_of_chain line 372
  66. theorem OAI.SourceBurnside.LocalSyntax.Skeleton.component_form line 400
  67. theorem OAI.SourceBurnside.LocalSyntax.Skeleton.region_unique_head line 407
  68. def OAI.SourceBurnside.LocalSyntax.Skeleton.RightClosedComponent line 425
  69. def OAI.SourceBurnside.LocalSyntax.Skeleton.LeftClosedComponent line 428
  70. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.decompose_pair_chain line 431
  71. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.closed_pair_chain line 461
  72. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.closed_right line 465
  73. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.closed_left line 472
  74. theorem OAI.SourceBurnside.LocalSyntax.Skeleton.closed_components line 479