OAI/Combinatorics/IndependentSets/Machines/MachineExpanderTableRows.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.singleStep line 14
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.sequence line 20
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.widen line 27
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.tableRowData line 33
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.tableRowData_finalValue line 37
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.tableRowData_frame0 line 41
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.tableRowData_finalFrame line 48
8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.rowAfterState line 61
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.rowAfterState_position line 67
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.caller_rowAfterState line 72
11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.preparedRowInTime line 76
12. structure OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.VertexSuffixRun line 105
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.suffixRun_aux line 119
14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.suffixInTime line 173
15. structure OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.VertexRun line 180
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.vertexInTime line 194