OAI/Combinatorics/IndependentSets/Machines/MachineAffineLookup.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineAffineLookup.Alphabet line 14
2. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineAffineLookup.Label line 16
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineAffineLookup.instruction line 21
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineAffineLookup.steps line 36
5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineAffineLookup.finalTapes line 41
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAffineLookup.initialTapes_eq_update line 46
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAffineLookup.affineLookupTrace line 66
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAffineLookup.steps_le line 94
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAffineLookup.steps_le_table line 102
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAffineLookup.finalTapes_other line 109
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAffineLookup.finalTapes_output line 115
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineAffineLookup.machine line 120