OAI/Combinatorics/IndependentSets/Machines/MachineExpanderRowLookup.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel line 13
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.scanPhaseLabel line 17
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.reversePhaseLabel line 20
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupPhasePort line 23
5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseAddress line 26
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseAddress_eq_rowIndex line 29
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupTape_injective line 37
8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes line 41
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_index line 46
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_work line 54
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_output line 60
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_other line 66
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_table line 73
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_restore line 79
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseTrace line 102
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseInTime line 124