OAI/Combinatorics/IndependentSets/Machines/Structural.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.extendedLabel line 13
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.extendedCfg line 17
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.extendedStmt line 22
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.stepAux_extended line 40
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.sourceMachine line 64
  6. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.Label line 75
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.cleanupLabel line 77
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.resetLabel line 80
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.cleanupEntry line 82
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.completedProgram line 85
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.completedMachine line 92
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.finiteAlphabet line 103
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.embeddedCfg line 108
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.step_simulation line 112
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.embedded_init line 128
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.finalTapes_eq line 133
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.haltList_eq line 144
  18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.cleanupExecution line 149
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.outputsInTime line 182
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.completedTime line 207
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.completedTime_eval line 212
  22. structure OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.TerminalRun line 219
  23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTime line 226
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTime_finite_alphabet line 246
  25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTimeOfEnumeration line 257