OAI/Combinatorics/IndependentSets/Machines/OldSelectSteps.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.oldSelectSteps line 13
  2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectOldTrace line 18
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps line 62
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps_eq line 66
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectDummyTrace line 71
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectionSteps line 130
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectionTrace line 138
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectionSteps_le line 170
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectorMachine line 191
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectionInTime line 202
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes line 222
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes line 224
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectTape line 226
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView line 244
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView_left line 253
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView_right line 261
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTape line 266
  18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorStateEquiv line 268
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectStateEquiv line 277
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreAfterCleanup line 284
  21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreInstruction line 288
  22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreInitialState line 302
  23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreMachine line 306
  24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreMemory line 317
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreMemory_update_output line 323
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes_injective line 331
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes_injective line 335
  28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreCleaned line 339
  29. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupSteps line 344
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTrace line 349