OAI/Combinatorics/IndependentSets/Machines/MachineExpanderTableProgram.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.ExtraTape line 11
2. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.(instance at line 15) line 15
3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.Tape line 19
4. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.Alphabet line 21
5. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.alphabetFintype line 25
6. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.OuterLabel line 28
7. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.(instance at line 32) line 32
8. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.Label line 36
9. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.Position line 37
10. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.State line 38
11. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.RowStatePrefix line 39
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.guardStates line 42
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.guardStates_apply line 49
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.guardStates_symm_apply line 53
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.rowFactor_pos line 56
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.zeroPosition line 60
17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.nextPosition line 63
18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.positionPair line 66
19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.caller line 69
20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.boundaryState line 71
21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.initialState line 76
22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.prepareState line 80
23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.resetState line 84
24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.clearRegister line 88
25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.advancePositionState line 91
26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.resetPositionState line 94
27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.vertexGuardCore line 97
28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.outerStatement line 107
29. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.rowReturn line 127
30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.program line 129
31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.program_row line 134
32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.program_outer line 140
33. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.rowExecution line 144
34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.rowExecution_steps line 156
35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.rowTapes line 164
36. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.extraTapes line 170
37. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes line 174
38. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.initialTapes line 178
39. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.finalTapes line 184