OAI/Combinatorics/IndependentSets/Machines/MachineSubroutine.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineSubroutine.label line 13
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineSubroutine.configuration line 17
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineSubroutine.statement line 20
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineSubroutine.stepAux_simulation line 34
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineSubroutine.step_simulation line 55
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineSubroutine.trace line 71
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineSubroutine.execution line 81
  8. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookup.Alphabet line 99
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookup.initialTapes line 101
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookup.finalTapes line 106
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookup.lookupFramedHaltTrace_some line 113
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookup.preservingLookupTrace line 131
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookup.preservingLookup_steps_le line 181
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookup.preservingLookupInTime line 189
  15. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookup.Label line 211
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookup.program line 215
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookup.machine line 222