OAI/Combinatorics/IndependentSets/Machines/MachineTableRows.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.Label line 13
  2. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.(instance at line 18) line 18
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.Alphabet line 25
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.routine line 27
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.fieldBits line 49
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.fieldSize line 52
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.fieldBits_length line 56
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.prefixTapes line 60
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.prefixTrace line 63
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.appendTrace line 115
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.rowBits_eq line 159
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.fieldBits_eq_rowBits line 165
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.timePolynomial line 173
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.timePolynomial_bounds line 176
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.rowAppendInTime line 183
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.machine line 208
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.machineRowInTime line 219
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableRows.outputFrame line 248