OAI/Combinatorics/IndependentSets/Expansion/PoweringRowData.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.firstMatch_of_first line 17
2. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.firstMatch_firstIndex line 27
3. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.endpointMask line 36
4. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.firstMatch_endpointMask line 40
5. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.slotCount line 50
6. abbrev OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.RowBuffer line 52
7. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.fixedLabelAt line 54
8. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.fixedLabelAt_addressIndex line 58
9. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.walkData line 66
10. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.walkBits line 76
11. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.basePredicate_walkBits line 80
12. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.leftMatches_walkBits line 87
13. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.rightMatches_walkBits line 94
14. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.firstMatch_walkBits_left line 102
15. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.firstMatch_walkBits_right line 112
16. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.edgeAccept_walkBits line 123
17. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.rowAccept_walkBits line 136
18. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.transposeField line 147
19. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.transposeBits line 152
20. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.basePredicate_transposeBits line 155
21. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.leftMatches_transposeBits line 160
22. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.rightMatches_transposeBits line 166
23. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.edgeAccept_transposeBits line 172
24. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.rowAccept_transposeBits line 181
25. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.rowBits line 188
26. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.rowData line 192
27. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.rowBits_packData line 197
28. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.rowBits_field line 204
29. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.rowAccept_rowBits line 211
30. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.rowBlock_at_rowBits line 221
31. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.dataWords line 229
32. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.dataTape line 233
33. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.dataTape_eq line 237
34. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.dataWords_length line 242
35. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.dataTape_length_le line 248
36. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.emittedRelation line 254
37. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.emittedRelation_eq line 259
38. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.rowBlock_unary line 267
39. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.emittedRelation_table line 279
40. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.rowBlock_unary_table line 306
41. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowData.tableRowMachineInTime line 313