OAI/GroupTheory/PeriodicGroups/Rules/Recognizer.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SourceBurnside.FiniteTable.Recognizer.firstTest line 11
2. lemma OAI.SourceBurnside.FiniteTable.Recognizer.firstTest_iff line 15
3. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideFirst line 17
4. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideLast line 20
5. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideAdmissible line 22
6. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideLeftExternal line 24
7. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideRightExternal line 26
8. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideAcceptsLeft line 28
9. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideAcceptsRight line 31
10. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideStructural line 34
11. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideInternal line 37
12. instance OAI.SourceBurnside.FiniteTable.Recognizer.decidePair line 40
13. def OAI.SourceBurnside.FiniteTable.Recognizer.paletteTest line 44
14. def OAI.SourceBurnside.FiniteTable.Recognizer.coreTest line 47
15. lemma OAI.SourceBurnside.FiniteTable.Recognizer.paletteTest_iff line 50
16. lemma OAI.SourceBurnside.FiniteTable.Recognizer.coreTest_iff line 52
17. instance OAI.SourceBurnside.FiniteTable.Recognizer.decidePalette line 54
18. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideCore line 57
19. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideHead line 60
20. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideEndpoint line 63
21. def OAI.SourceBurnside.FiniteTable.Recognizer.dataTest line 67
22. lemma OAI.SourceBurnside.FiniteTable.Recognizer.dataTest_iff line 71
23. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideDataTest line 74
24. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideFormat line 78
25. def OAI.SourceBurnside.FiniteTable.Recognizer.UnaryTest line 82
26. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideUnaryTest line 107
27. lemma OAI.SourceBurnside.FiniteTable.Recognizer.unary_test line 111
28. lemma OAI.SourceBurnside.FiniteTable.Recognizer.unary_of_test line 115
29. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideUnary line 133
30. def OAI.SourceBurnside.FiniteTable.Recognizer.headfreeTest line 136
31. lemma OAI.SourceBurnside.FiniteTable.Recognizer.headfreeTest_iff line 141
32. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideHeadFree line 143
33. def OAI.SourceBurnside.FiniteTable.Recognizer.AcquireTest line 147
34. def OAI.SourceBurnside.FiniteTable.Recognizer.ReadLeftTest line 152
35. def OAI.SourceBurnside.FiniteTable.Recognizer.ReadRightTest line 158
36. def OAI.SourceBurnside.FiniteTable.Recognizer.UndoLeftTest line 163
37. def OAI.SourceBurnside.FiniteTable.Recognizer.UndoRightTest line 168
38. def OAI.SourceBurnside.FiniteTable.Recognizer.CheckerCreateTest line 174
39. def OAI.SourceBurnside.FiniteTable.Recognizer.CheckerAdvanceTest line 179
40. def OAI.SourceBurnside.FiniteTable.Recognizer.SwapTest line 184
41. def OAI.SourceBurnside.FiniteTable.Recognizer.BinaryTest line 188
42. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideAcquireTest line 193
43. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideReadLeftTest line 195
44. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideReadRightTest line 197
45. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideUndoLeftTest line 199
46. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideUndoRightTest line 201
47. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideCheckerCreateTest line 203
48. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideCheckerAdvanceTest line 205
49. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideSwapTest line 207
50. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideBinaryTest line 209
51. lemma OAI.SourceBurnside.FiniteTable.Recognizer.checkerCreateTest_iff line 212
52. lemma OAI.SourceBurnside.FiniteTable.Recognizer.checkerAdvanceTest_iff line 217
53. lemma OAI.SourceBurnside.FiniteTable.Recognizer.swapTest_iff line 222
54. lemma OAI.SourceBurnside.FiniteTable.Recognizer.binary_test line 227
55. lemma OAI.SourceBurnside.FiniteTable.Recognizer.binary_of_test line 257
56. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideBinary line 282
57. def OAI.SourceBurnside.FiniteTable.Recognizer.palettePairTest line 285
58. lemma OAI.SourceBurnside.FiniteTable.Recognizer.palettePairTest_iff line 293
59. instance OAI.SourceBurnside.FiniteTable.Recognizer.decidePalettePair line 301
60. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideLastOK line 306
61. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideCheckerPair line 308
62. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideCellPair line 311
63. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideSemanticZero line 314
64. def OAI.SourceBurnside.FiniteTable.Recognizer.passedOwnColorTest line 318
65. lemma OAI.SourceBurnside.FiniteTable.Recognizer.passedOwnColorTest_iff line 321
66. instance OAI.SourceBurnside.FiniteTable.Recognizer.decidePassedOwnColor line 324
67. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideUnaryZero line 330
68. def OAI.SourceBurnside.FiniteTable.Recognizer.duplicateColorTest line 334
69. lemma OAI.SourceBurnside.FiniteTable.Recognizer.duplicateColorTest_iff line 337
70. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideDuplicateColor line 340
71. def OAI.SourceBurnside.FiniteTable.Recognizer.missingColorTest line 347
72. lemma OAI.SourceBurnside.FiniteTable.Recognizer.missingColorTest_iff line 350
73. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideMissingColor line 353
74. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideBinaryZero line 359
75. def OAI.SourceBurnside.FiniteTable.Recognizer.ReplacementTest line 363
76. lemma OAI.SourceBurnside.FiniteTable.Recognizer.replacementTest_iff line 370
77. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideReplacement line 375
78. def OAI.SourceBurnside.FiniteTable.Recognizer.ZeroTest line 382
79. lemma OAI.SourceBurnside.FiniteTable.Recognizer.zeroTest_iff line 387
80. instance OAI.SourceBurnside.FiniteTable.Recognizer.decideZero line 394
81. instance OAI.SourceBurnside.FiniteTable.Codec.decideRawUnaryZero line 406
82. instance OAI.SourceBurnside.FiniteTable.Codec.decideRawBinaryZero line 410
83. instance OAI.SourceBurnside.FiniteTable.Codec.decideRawReplacement line 414
84. instance OAI.SourceBurnside.FiniteTable.Codec.decideRawZero line 418
85. def OAI.SourceBurnside.FiniteTable.Codec.entry line 423
86. lemma OAI.SourceBurnside.FiniteTable.Codec.entry_zero line 426
87. lemma OAI.SourceBurnside.FiniteTable.Codec.entry_replacement line 428
88. def OAI.SourceBurnside.FiniteTable.Codec.binaryValue line 435
89. lemma OAI.SourceBurnside.FiniteTable.Codec.binaryValue_bit line 436
90. lemma OAI.SourceBurnside.FiniteTable.Codec.binaryValue_lt line 439
91. def OAI.SourceBurnside.FiniteTable.Codec.natCode line 441
92. lemma OAI.SourceBurnside.FiniteTable.Codec.natCode_lt line 442
93. lemma OAI.SourceBurnside.FiniteTable.Codec.natCode_bit line 443
94. lemma OAI.SourceBurnside.FiniteTable.Codec.natCode_injective line 445
95. lemma OAI.SourceBurnside.FiniteTable.Codec.readInt_arithmetic line 450
96. lemma OAI.SourceBurnside.FiniteTable.Codec.readFlag_arithmetic line 470
97. lemma OAI.SourceBurnside.FiniteTable.Codec.flag_as_nat line 475
98. lemma OAI.SourceBurnside.FiniteTable.Codec.getFin_eq_some_iff line 484
99. lemma OAI.SourceBurnside.FiniteTable.Codec.getPosition_eq_some_iff line 495
100. lemma OAI.SourceBurnside.FiniteTable.Codec.getMarker_eq_some_iff line 500
101. lemma OAI.SourceBurnside.FiniteTable.Codec.getChecker_eq_some_iff line 503
102. lemma OAI.SourceBurnside.FiniteTable.Codec.getPhase_eq_some_iff line 508
103. lemma OAI.SourceBurnside.FiniteTable.Codec.getFin_isSome line 511
104. lemma OAI.SourceBurnside.FiniteTable.Codec.getPosition_isSome line 512
105. lemma OAI.SourceBurnside.FiniteTable.Codec.getMarker_isSome line 516
106. lemma OAI.SourceBurnside.FiniteTable.Codec.getChecker_isSome line 519
107. lemma OAI.SourceBurnside.FiniteTable.Codec.getPhase_isSome line 523
108. def OAI.SourceBurnside.FiniteTable.Codec.UsedAgree line 527
109. lemma OAI.SourceBurnside.FiniteTable.Codec.parse_used line 531
110. def OAI.SourceBurnside.FiniteTable.Codec.InRange line 550
111. lemma OAI.SourceBurnside.FiniteTable.Codec.integers_inRange line 555
112. lemma OAI.SourceBurnside.FiniteTable.Codec.parse_isSome line 565
113. lemma OAI.SourceBurnside.FiniteTable.Codec.integers_unused line 587
114. lemma OAI.SourceBurnside.FiniteTable.Codec.flags_unused line 590
115. def OAI.SourceBurnside.FiniteTable.Codec.usedWrite line 594
116. lemma OAI.SourceBurnside.FiniteTable.Codec.usedWrite_of_parse line 598
117. lemma OAI.SourceBurnside.FiniteTable.Codec.decode_isSome_by_fields line 612
118. lemma OAI.SourceBurnside.FiniteTable.Codec.readInt_bit line 626
119. def OAI.SourceBurnside.FiniteTable.Codec.ReservedZero line 633
120. lemma OAI.SourceBurnside.FiniteTable.Codec.usedWrite_reserved line 636
121. lemma OAI.SourceBurnside.FiniteTable.Codec.usedWrite_eq_of_reserved line 652
122. lemma OAI.SourceBurnside.FiniteTable.Codec.canonical_iff_reserved line 688
123. lemma OAI.SourceBurnside.FiniteTable.Codec.zero_window line 695
124. lemma OAI.SourceBurnside.FiniteTable.Codec.zero_high line 709
125. lemma OAI.SourceBurnside.FiniteTable.Codec.reserved_arithmetic line 719
126. lemma OAI.SourceBurnside.FiniteTable.Codec.decode_isSome_arithmetic line 746