OAI/Combinatorics/IndependentSets/Machines/MachineDummyRows.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.trueRelation line 13
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.trueBits line 15
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.trueBits_length line 17
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.rowBits line 23
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.rowBits_length line 25
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.rowBits_eq_graph_row line 29
7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.rowsBits line 34
8. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.Label line 38
9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.start line 40
10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.rowLabel line 41
11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.bumpLabel line 43
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.fields line 45
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.afterPort line 47
14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.entry line 50
15. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.Alphabet line 55
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.continueAt line 57
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.stepAux_continueAt line 63
18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.program line 68
19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.fieldTapes line 75
20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.initialTapes line 78
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.initializeStep line 81
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.rowTrace line 94
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.bumpStep line 115
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.rowAndBumpTrace line 126
25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.steps line 137
26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.suffixTrace line 142
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.allTrace line 165
28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.graphRows line 180
29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.graphRows_length line 187
30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.rowsBits_eq_graphRows line 193
31. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.dummyRows line 203
32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.dummyRows_length line 208
33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.dummyRowsTrace line 211
34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.steps_le_bound line 223
35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.inputSize line 255
36. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.timePolynomial line 258
37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.timePolynomial_bounds line 264
38. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.machine line 285
39. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.machineInTime line 296
40. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.machineDummyInTime line 307
41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDummyRows.finalFrame line 320