OAI/Computability/DirectedFeedback/Probability/PoweringFieldPlan.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.tailPorts line 58
2. theorem OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.tailPorts_length line 62
3. theorem OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.walkEnd_tailPorts line 72
4. def OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.headPorts line 83
5. theorem OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.walkEnd_headPorts line 86
6. def OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.addressPorts line 94
7. theorem OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.walkEnd_addressPorts line 97
8. inductive OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.Instruction line 102
9. def OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.Instruction.radius line 106
10. theorem OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.addressPorts_length_le line 110
11. def OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.evaluate line 115
12. def OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.fieldPlan line 123
13. theorem OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.evaluate_fieldPlan line 129
14. def OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.directedFieldPlan line 149
15. theorem OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.fieldPlan_radius line 153
16. theorem OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.directedFieldPlan_radius line 168
17. theorem OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.evaluate_directedFieldPlan line 173
18. def OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.rowPlan line 180
19. theorem OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.evaluate_rowPlan line 186
20. theorem OAI.DFVSGames.Foundations.PCP.PoweringFieldPlan.dataTape_eq_plan line 197
21. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.Tape line 214
22. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.State line 215
23. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.Label line 217
24. instance OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.labelFintype line 221
25. instance OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.labelDecidableEq line 224
26. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.entry line 227
27. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.instruction line 231
28. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.finalTapes line 240
29. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.steps line 250
30. structure OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.Ready line 254
31. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.finalTapes_role line 262
32. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.ready_finalTapes line 277
33. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.finalTapes_other line 294
34. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.fieldTrace line 307
35. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineField.finalTapes_output line 329
36. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.Command line 364
37. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.LocalLabel line 365
38. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.Label line 366
39. def OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.entry line 368
40. def OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.instruction line 372
41. def OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.result line 379
42. def OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.finalTapes line 383
43. def OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.steps line 387
44. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.planTrace line 392
45. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.ready_finalTapes line 418
46. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.finalTapes_output line 431
47. def OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan line 452
48. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan_values line 459
49. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachinePlan.rowPlan_output line 464
50. def OAI.DFVSGames.Foundations.Complexity.PoweringPlanBudget.fieldBudget line 489
51. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPlanBudget.field_steps_le line 492
52. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPlanBudget.plan_steps_le line 517
53. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPlanBudget.boundedRowPlan_length line 534
54. def OAI.DFVSGames.Foundations.Complexity.PoweringPlanBudget.rowBudget line 540
55. theorem OAI.DFVSGames.Foundations.Complexity.PoweringPlanBudget.rowPlan_steps_le line 544
56. def OAI.DFVSGames.Foundations.Complexity.PoweringPlanBudget.planInTime line 557
57. def OAI.DFVSGames.Foundations.Complexity.PoweringPlanBudget.rowPlanInTime line 576
58. def OAI.DFVSGames.Foundations.PCP.PoweringRowHeaderSemantics.blockSize line 614
59. def OAI.DFVSGames.Foundations.PCP.PoweringRowHeaderSemantics.reverseOffset line 616
60. def OAI.DFVSGames.Foundations.PCP.PoweringRowHeaderSemantics.reverseValue line 619
61. def OAI.DFVSGames.Foundations.PCP.PoweringRowHeaderSemantics.tailVertex line 623
62. def OAI.DFVSGames.Foundations.PCP.PoweringRowHeaderSemantics.headerWords line 627
63. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowHeaderSemantics.table_tail line 631
64. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowHeaderSemantics.table_reverseValue line 643
65. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowHeaderSemantics.headerWords_eq line 653
66. theorem OAI.DFVSGames.Foundations.PCP.PoweringRowHeaderSemantics.header_relation_bits line 663
67. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement line 690
68. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_injective line 693
69. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_table line 697
70. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_query line 701
71. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_scan line 705
72. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_reverse line 709
73. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_scratch line 713
74. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_output line 717
75. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_start line 721
76. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.headerPlacement_succ line 725
77. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.Label line 729
78. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.entry line 732
79. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.tailEntry line 734
80. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.affineInstruction line 737
81. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.instruction line 744
82. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.afterReverse line 757
83. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes line 762
84. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.steps line 771
85. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.headerTrace line 777
86. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes_other line 849
87. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.finalTapes_shared line 872
88. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.steps_le line 886
89. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowHeaders.machine line 902