OAI/Combinatorics/IndependentSets/Machines/MachineExpanderTableBoundary.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.caller_boundaryState line 13
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.prepareState_boundaryState line 17
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.clearRegister_boundaryState line 22
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.caller_prepareState line 27
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.caller_resetState line 30
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.caller_clearRegister line 33
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.caller_advancePositionState line 36
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.caller_resetPositionState line 39
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.nextPosition_val_of_lt line 42
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_update_count line 46
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_increment_vertex line 56
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.initialTapes_initialize line 69
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.initializeStep line 83
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.initialize_boundaryStep line 92
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_succStep line 107
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_zeroStep line 119
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_boundary_succStep line 130
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_boundary_zeroStep line 143
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.prepareRowStep line 153
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.afterRow_moreStep line 161
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.afterRow_lastStep line 170
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.afterRow_last_boundaryStep line 180
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.reverseOutput_consStep line 199
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.reverseOutput_nilStep line 211
25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.doneStep line 223