OAI/Computability/DirectedFeedback/Machines/MachineExpanderRow.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.concatenate_inline_MachineExpanderRow line 56
2. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.rowSteps line 60
3. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.rowTraceAt line 78
4. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.rowSteps_le line 202
5. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.rowInTimeAt line 220
6. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.rowInTime line 235
7. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.caller_boundaryState line 256
8. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.prepareState_boundaryState line 260
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.clearRegister_boundaryState line 265
10. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.caller_prepareState line 270
11. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.caller_resetState line 273
12. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.caller_clearRegister line 276
13. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.caller_advancePositionState line 279
14. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.caller_resetPositionState line 282
15. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.nextPosition_val_of_lt line 285
16. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_update_count line 289
17. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_increment_vertex line 299
18. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.initialTapes_initialize line 312
19. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.initializeStep line 326
20. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.initialize_boundaryStep line 335
21. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_succStep line 350
22. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_zeroStep line 362
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_boundary_succStep line 373
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_boundary_zeroStep line 386
25. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.prepareRowStep line 396
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.afterRow_moreStep line 404
27. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.afterRow_lastStep line 413
28. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.afterRow_last_boundaryStep line 423
29. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.reverseOutput_consStep line 442
30. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.reverseOutput_nilStep line 454
31. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.doneStep line 466
32. def OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.globalIndex line 486
33. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.globalIndex_val line 492
34. def OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.rowValue line 505
35. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.rowValue_eq_reverseIndex line 511
36. def OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords line 518
37. def OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords line 521
38. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_length line 524
39. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_succ line 528
40. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_full line 535
41. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.vertexWords_drop_last line 540
42. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.ofFn_cast_inline_ExpanderTableEnumeration line 546
43. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.rotationWords_eq_ofFn line 551
44. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.rowCount_eq line 559
45. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords_eq_flat_ofFn line 562
46. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords_eq_rotationWords line 580
47. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.generatedWords_length line 587
48. def OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices line 592
49. def OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows line 595
50. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices_zero line 599
51. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices_full line 602
52. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.priorVertices_succ line 607
53. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows_zero line 614
54. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows_succ line 618
55. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.prefixRows_complete line 626
56. def OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.accumulate line 632
57. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_eq line 635
58. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_append line 643
59. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_prefixRows_succ line 647
60. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_generatedWords line 655
61. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.encode_generatedWords_length_le line 661
62. theorem OAI.DFVSGames.Foundations.PCP.ExpanderTableEnumeration.accumulate_generatedWords_length_le line 667
63. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.singleStep_inline_MachineExpanderTableRows line 686
64. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.sequence_inline_MachineExpanderTableRows line 692
65. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.widen_inline_MachineExpanderTableRows line 699
66. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.tableRowData line 705
67. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.tableRowData_finalValue line 709
68. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.tableRowData_frame0 line 713
69. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.tableRowData_finalFrame line 720
70. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.rowAfterState line 733
71. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.rowAfterState_position line 739
72. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.caller_rowAfterState line 744
73. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.preparedRowInTime line 748
74. structure OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.VertexSuffixRun line 777
75. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.suffixRun_aux_inline_MachineExpanderTableRows line 791
76. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.suffixInTime line 845
77. structure OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.VertexRun line 852
78. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.vertexInTime line 866