OAI/Computability/MinUncut/Machines/PoweringMachineRow.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.Field line 13
2. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.inputSize line 15
3. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.fieldEquiv line 17
4. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.inputEquiv line 21
5. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.packData line 24
6. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.packData_inputEquiv line 27
7. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.basePredicate line 32
8. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.leftMatches line 36
9. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.rightMatches line 40
10. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.firstMatch line 44
11. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.firstMatch_spec line 47
12. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.firstMatch_none line 54
13. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.edgeAccept line 58
14. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.edgeAccept_of_matches line 64
15. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.rowAccept line 72
16. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.rowAccept_eq_true line 76
17. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.rowBlock line 82
18. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.rowBlock_at line 88
19. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.encodeBit line 95
20. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.encodeBits line 97
21. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.encodeBits_append line 101
22. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.encodeBits_graphWords line 107
23. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.encodeBits_length_le line 114
24. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.readEncodedSlots line 126
25. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.stepAux_readEncodedSlots line 139
26. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.stepAux_readEncodedAll line 158
27. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_readEncodedSlots line 174
28. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.writeEncodedSlots line 182
29. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.stepAux_writeEncodedSlots line 190
30. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_writeEncodedSlots line 207
31. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.encodedBlockStmt line 224
32. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.encodedBlockAt line 231
33. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_encodedBlockAt line 235
34. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.stepAux_encodedBlockStmt line 244
35. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.stepAux_encodedBlockAt line 259
36. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.step_encodedBlockAt line 270
37. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.rowAt line 287
38. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.machine line 292
39. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.machine_statementPushBound line 303
40. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRow.machineInTime line 308
41. inductive OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape line 338
42. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape.enumList line 342
43. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape.enumList_getElem?_ctorIdx_eq line 344
44. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape.enumList_nodup line 348
45. instance OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.(instance at line 350) line 350
46. inductive OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel line 354
47. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel.enumList line 358
48. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel.enumList_getElem?_ctorIdx_eq line 360
49. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel.enumList_nodup line 364
50. instance OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.(instance at line 366) line 366
51. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.HeaderAlphabet line 370
52. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.HeaderState line 371
53. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.pushTrue line 373
54. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.stepAux_pushTrue line 378
55. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.pushTrue_pushBound line 390
56. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.headerProgram line 398
57. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.headerMachine line 414
58. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.initialTapes line 425
59. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.scanTapes line 429
60. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.finalTapes line 435
61. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.scanConfiguration line 441
62. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.finalConfiguration line 446
63. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.initializeStep line 450
64. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.scanStep_zero line 460
65. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.scanStep_succ line 471
66. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.scanTrace line 488
67. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.headerTrace line 505
68. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.headerInTime line 517
69. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.remainingRows line 526
70. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.remainingRows_top line 529
71. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.remainingRows_step line 532
72. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.rowBase line 541
73. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.VertexBodyTraces line 545
74. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.vertexBodyTraces_to_counted line 558
75. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.vertexLoopInTime line 571
76. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.vertexLoop_output line 594
77. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.varyingRowBase line 600
78. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.VaryingVertexBodyTraces line 604
79. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.varyingVertexBodyTraces_to_counted line 617
80. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.vertexLoopInTime_varying line 630
81. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineLoop.vertexLoop_varying_output line 653