OAI/Computability/MinUncut/PCP/PoweringRowData.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.firstMatch_of_first line 17
2. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.firstMatch_firstIndex line 27
3. def OAI.MinUncutGames.Foundations.PCP.PoweringRowData.endpointMask line 36
4. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.firstMatch_endpointMask line 40
5. def OAI.MinUncutGames.Foundations.PCP.PoweringRowData.slotCount line 50
6. abbrev OAI.MinUncutGames.Foundations.PCP.PoweringRowData.RowBuffer line 52
7. def OAI.MinUncutGames.Foundations.PCP.PoweringRowData.fixedLabelAt line 54
8. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.fixedLabelAt_addressIndex line 58
9. def OAI.MinUncutGames.Foundations.PCP.PoweringRowData.walkData line 66
10. def OAI.MinUncutGames.Foundations.PCP.PoweringRowData.walkBits line 76
11. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.basePredicate_walkBits line 80
12. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.leftMatches_walkBits line 87
13. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.rightMatches_walkBits line 94
14. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.firstMatch_walkBits_left line 102
15. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.firstMatch_walkBits_right line 112
16. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.edgeAccept_walkBits line 123
17. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.rowAccept_walkBits line 136
18. def OAI.MinUncutGames.Foundations.PCP.PoweringRowData.transposeField line 147
19. def OAI.MinUncutGames.Foundations.PCP.PoweringRowData.transposeBits line 152
20. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.basePredicate_transposeBits line 155
21. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.leftMatches_transposeBits line 160
22. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.rightMatches_transposeBits line 166
23. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.edgeAccept_transposeBits line 172
24. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.rowAccept_transposeBits line 181
25. def OAI.MinUncutGames.Foundations.PCP.PoweringRowData.rowBits line 188
26. def OAI.MinUncutGames.Foundations.PCP.PoweringRowData.rowData line 192
27. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.rowBits_packData line 197
28. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.rowBits_field line 204
29. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.rowAccept_rowBits line 211
30. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.rowBlock_at_rowBits line 221
31. def OAI.MinUncutGames.Foundations.PCP.PoweringRowData.dataWords line 229
32. def OAI.MinUncutGames.Foundations.PCP.PoweringRowData.dataTape line 233
33. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.dataTape_eq line 237
34. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.dataWords_length line 242
35. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.dataTape_length_le line 248
36. def OAI.MinUncutGames.Foundations.PCP.PoweringRowData.emittedRelation line 254
37. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.emittedRelation_eq line 259
38. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.rowBlock_unary line 267
39. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.emittedRelation_table line 279
40. theorem OAI.MinUncutGames.Foundations.PCP.PoweringRowData.rowBlock_unary_table line 306
41. def OAI.MinUncutGames.Foundations.PCP.PoweringRowData.tableRowMachineInTime line 313
42. def OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.tailPorts line 341
43. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.tailPorts_length line 345
44. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.walkEnd_tailPorts line 355
45. def OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.headPorts line 366
46. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.walkEnd_headPorts line 369
47. def OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.addressPorts line 377
48. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.walkEnd_addressPorts line 380
49. inductive OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.Instruction line 385
50. def OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.Instruction.radius line 389
51. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.addressPorts_length_le line 393
52. def OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.evaluate line 398
53. def OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.fieldPlan line 406
54. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.evaluate_fieldPlan line 412
55. def OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.directedFieldPlan line 432
56. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.fieldPlan_radius line 436
57. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.directedFieldPlan_radius line 451
58. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.evaluate_directedFieldPlan line 456
59. def OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.rowPlan line 463
60. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.evaluate_rowPlan line 469
61. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFieldPlan.dataTape_eq_plan line 480