OAI/GroupTheory/PeriodicGroups/Formulas/PredicateCompilation.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SourceBurnside.PredicateFormula.rawBinaryRep_exact line 11
2. def OAI.SourceBurnside.PredicateFormula.normalEntry line 31
3. lemma OAI.SourceBurnside.PredicateFormula.normalEntry_zero_one line 38
4. lemma OAI.SourceBurnside.PredicateFormula.normalEntry_zero_two line 44
5. lemma OAI.SourceBurnside.PredicateFormula.normalEntry_rep_one line 50
6. lemma OAI.SourceBurnside.PredicateFormula.normalEntry_rep_two line 56
7. lemma OAI.SourceBurnside.PredicateFormula.normalEntry_other line 65
8. def OAI.SourceBurnside.Structured.Device.Formula.totalize line 75
9. theorem OAI.SourceBurnside.Structured.Device.Formula.totalize_eval line 87
10. def OAI.SourceBurnside.Structured.Device.Formula.Bounded line 113
11. lemma OAI.SourceBurnside.Structured.Device.Formula.compare_boolean line 124
12. lemma OAI.SourceBurnside.Structured.Device.Formula.totalize_safe line 127
13. lemma OAI.SourceBurnside.Structured.Device.Formula.bounded_mono line 180
14. def OAI.SourceBurnside.Structured.Device.Formula.Exponents line 200
15. def OAI.SourceBurnside.Structured.Device.Formula.weight line 206
16. lemma OAI.SourceBurnside.Structured.Device.Formula.weight_pos line 212
17. lemma OAI.SourceBurnside.Structured.Device.Formula.width_pos line 213
18. lemma OAI.SourceBurnside.Structured.Device.Formula.bound_pow_mono line 214
19. lemma OAI.SourceBurnside.Structured.Device.Formula.width_binary line 216
20. lemma OAI.SourceBurnside.Structured.Device.Formula.binary_value_bound line 218
21. theorem OAI.SourceBurnside.Structured.Device.Formula.bounded_of_exponents line 229
22. theorem OAI.SourceBurnside.Structured.Device.Formula.timed_total line 308
23. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_constant line 322
24. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_read line 323
25. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_branch line 324
26. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_equal line 327
27. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_less line 330
28. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_neg line 333
29. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_and line 335
30. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_or line 337
31. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_implies line 339
32. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_all line 341
33. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_any line 345
34. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_bit line 349
35. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_field line 351
36. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_bind line 353
37. lemma OAI.SourceBurnside.RawFormula.valid_exponents line 372
38. lemma OAI.SourceBurnside.PredicateFormula.valid_exponents line 416
39. def OAI.SourceBurnside.CellFormula.Exponents line 426
40. lemma OAI.SourceBurnside.CellFormula.ofRaw_exponents line 428
41. def OAI.SourceBurnside.AddressFormula.Exponents line 452
42. lemma OAI.SourceBurnside.AddressFormula.certificate_exponents line 453
43. lemma OAI.SourceBurnside.AddressFormula.data_exponents line 455
44. def OAI.SourceBurnside.InitialFormula.Expr.Exponents line 462
45. lemma OAI.SourceBurnside.InitialFormula.fixed_exponents line 464
46. lemma OAI.SourceBurnside.InitialFormula.data_exponents line 466
47. lemma OAI.SourceBurnside.InitialFormula.choose_exponents line 468
48. lemma OAI.SourceBurnside.InitialFormula.symbol_exponents line 482
49. def OAI.SourceBurnside.InitialFormula.Piece.Exponents line 491
50. lemma OAI.SourceBurnside.InitialFormula.Piece.append_exponents line 493
51. lemma OAI.SourceBurnside.InitialFormula.fixedBits_exponents line 507
52. lemma OAI.SourceBurnside.InitialFormula.number_exponents line 513
53. lemma OAI.SourceBurnside.InitialFormula.ones_exponents line 524
54. lemma OAI.SourceBurnside.InitialFormula.header_exponents line 526
55. lemma OAI.SourceBurnside.InitialFormula.bits_exponents line 530
56. lemma OAI.SourceBurnside.InitialFormula.single_exponents line 535
57. lemma OAI.SourceBurnside.InitialFormula.dataPiece_exponents line 537
58. lemma OAI.SourceBurnside.InitialFormula.inputPiece_exponents line 542
59. lemma OAI.SourceBurnside.InitialFormula.cell_exponents line 557
60. lemma OAI.SourceBurnside.CellFormula.equalCells_exponents line 578
61. lemma OAI.SourceBurnside.CellFormula.wing_exponents line 589
62. lemma OAI.SourceBurnside.CellFormula.boundary_exponents line 591
63. lemma OAI.SourceBurnside.CellFormula.full_exponents line 595
64. lemma OAI.SourceBurnside.CellFormula.idle_exponents line 599
65. lemma OAI.SourceBurnside.CellFormula.setChecker_exponents line 604
66. lemma OAI.SourceBurnside.CellFormula.setColor_exponents line 608
67. lemma OAI.SourceBurnside.CellFormula.formats_exponents line 612
68. lemma OAI.SourceBurnside.CellFormula.pair_exponents line 618
69. lemma OAI.SourceBurnside.CellFormula.unaryZero_exponents line 624
70. lemma OAI.SourceBurnside.CellFormula.binaryZero_exponents line 630
71. lemma OAI.SourceBurnside.AddressFormula.readAt_exponents line 641
72. def OAI.SourceBurnside.ClauseFormula.Expr.Exponents line 650
73. lemma OAI.SourceBurnside.ClauseFormula.matchReg_exponents line 652
74. lemma OAI.SourceBurnside.ClauseFormula.truth_exponents line 658
75. lemma OAI.SourceBurnside.ClauseFormula.delta_exponents line 664
76. lemma OAI.SourceBurnside.ClauseFormula.choose_exponents line 667
77. lemma OAI.SourceBurnside.ClauseFormula.lookup_exponents line 670
78. lemma OAI.SourceBurnside.ClauseFormula.truthTable_exponents line 678
79. def OAI.SourceBurnside.ClauseFormula.ReadingExpr.Exponents line 682
80. lemma OAI.SourceBurnside.ClauseFormula.fixedReading_exponents line 684
81. lemma OAI.SourceBurnside.ClauseFormula.addressReading_exponents line 686
82. lemma OAI.SourceBurnside.ClauseFormula.make_exponents line 688
83. lemma OAI.SourceBurnside.ClauseFormula.unit_exponents line 691
84. lemma OAI.SourceBurnside.ClauseFormula.equalReading_exponents line 694
85. lemma OAI.SourceBurnside.ClauseFormula.initialData_exponents line 698
86. lemma OAI.SourceBurnside.ClauseFormula.wire_exponents line 705
87. lemma OAI.SourceBurnside.ClauseFormula.circuitClause_exponents line 710
88. lemma OAI.SourceBurnside.InitialFormula.clauses_exponents line 718
89. lemma OAI.SourceBurnside.PhysicalFormula.x_exponents line 728
90. lemma OAI.SourceBurnside.PhysicalFormula.y_exponents line 733
91. lemma OAI.SourceBurnside.PhysicalFormula.localAddress_exponents line 738
92. lemma OAI.SourceBurnside.PhysicalFormula.localClause_exponents line 746
93. lemma OAI.SourceBurnside.PhysicalFormula.clauseIndex_exponents line 764
94. lemma OAI.SourceBurnside.PhysicalFormula.fallback_exponents line 768
95. lemma OAI.SourceBurnside.PhysicalFormula.initialFamily_exponents line 770
96. lemma OAI.SourceBurnside.PhysicalFormula.boundaryFamily_exponents line 777
97. lemma OAI.SourceBurnside.PhysicalFormula.finalFamily_exponents line 791
98. lemma OAI.SourceBurnside.PhysicalFormula.familyClause_exponents line 798
99. lemma OAI.SourceBurnside.PhysicalFormula.clauseAt_exponents line 810
100. lemma OAI.SourceBurnside.CellFormula.skeletonPair_exponents line 821
101. lemma OAI.SourceBurnside.CellFormula.register_exponents line 827
102. lemma OAI.SourceBurnside.CellFormula.zeroReg_exponents line 829
103. lemma OAI.SourceBurnside.CellFormula.unaryMove_exponents line 832
104. lemma OAI.SourceBurnside.CellFormula.addReg_exponents line 845
105. lemma OAI.SourceBurnside.CellFormula.binaryMove_exponents line 849
106. lemma OAI.SourceBurnside.InitialFormula.binSize_le_self line 876
107. def OAI.SourceBurnside.CellFormula.Ready line 886
108. lemma OAI.SourceBurnside.CellFormula.ofRaw_ready line 888
109. def OAI.SourceBurnside.PredicateFormula.Table.Exponents line 905
110. lemma OAI.SourceBurnside.PredicateFormula.Table.truth_exponents line 908
111. lemma OAI.SourceBurnside.PredicateFormula.Table.delta_exponents line 911
112. lemma OAI.SourceBurnside.PredicateFormula.clauseCount_exponents line 915
113. lemma OAI.SourceBurnside.PredicateFormula.physical_exponents line 918
114. lemma OAI.SourceBurnside.PredicateFormula.unaryRep_exponents line 941
115. lemma OAI.SourceBurnside.PredicateFormula.binaryRep_exponents line 953
116. lemma OAI.SourceBurnside.PredicateFormula.rawUnaryZero_exponents line 974
117. lemma OAI.SourceBurnside.PredicateFormula.rawBinaryZero_exponents line 980
118. lemma OAI.SourceBurnside.PredicateFormula.rawUnaryRep_exponents line 986
119. lemma OAI.SourceBurnside.PredicateFormula.rawBinaryRep_exponents line 992
120. lemma OAI.SourceBurnside.PredicateFormula.normalEntry_exponents line 1007
121. def OAI.SourceBurnside.Structured.Device.packed line 1025
122. lemma OAI.SourceBurnside.Structured.Device.packed_length line 1026
123. lemma OAI.SourceBurnside.Structured.Device.packed_value line 1029
124. def OAI.SourceBurnside.Structured.Device.packedInputs line 1032
125. lemma OAI.SourceBurnside.Structured.Device.packedInputs_values line 1033
126. lemma OAI.SourceBurnside.Structured.Device.packedInputs_lengths line 1035