OAI/Combinatorics/IndependentSets/Machines/CoreInputTapes.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreCleaned_memory line 12
  2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupSteps_memory line 20
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorFinalFrame line 32
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTrace line 48
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectFrame line 94
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectionTrace line 103
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTrace line 138
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreInputTapes line 170
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreSteps line 180
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreTrace line 194
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectedIndex_le line 241
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.encodedDrop_length_le line 252
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.rotorSize_le_encodedLength line 259
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreTimeBound line 267
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreSteps_le line 271
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreMachineInTime line 335