OAI/Combinatorics/IndependentSets/Machines/Alphabet.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.Alphabet line 19
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.equalityBits line 21
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.equalityBits_length_le line 24
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits line 27
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits_length line 30
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits_eq_row line 35
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation line 49
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation_div line 56
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation_mod line 64
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.rotationLookupTrace line 73
11. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.FinishLabel line 96
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.finishFields line 102
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_zero line 106
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_one line 108
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_two line 110
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.finishInstruction line 112
17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.finishSteps line 131
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.finishSteps_le line 136
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.joinTrace line 143
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.finishTrace line 147
21. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.RotorLabel line 262
22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes line 267
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes_injective line 271
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes_outside line 279
25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.rotorInstruction line 286
26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.rotorFinalTapes line 297
27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.rotorSteps line 307
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.rotorTrace line 312
29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.rotorSteps_le line 391
30. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape line 401
31. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 406) line 406
32. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.SelectTape line 411
33. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.RawSelectAlphabet line 412