OAI/Combinatorics/IndependentSets/Machines/MachineRegularOwnerCleanup.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.Tape line 13
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.State line 14
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.Alphabet line 15
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.sumDecidableEq line 17
  5. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeDecidableEq line 28
  6. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeBEq line 40
  7. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeLawfulBEq line 43
  8. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeFintype line 47
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.core line 54
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.localRank line 55
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.count line 56
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.prefixTape line 57
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.rotor line 58
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.padding line 59
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.level line 60
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.dummyFuel line 61
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.scratch line 62
  18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupTapes line 64
  19. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.Label line 66
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.entry line 72
  21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupEntry line 74
  22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.instruction line 77
  23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.afterAddition line 86
  24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes line 89
  25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.steps line 92
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_apply line 95
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_prefix line 102
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_empty line 107
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_other line 111
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_scratch line 116
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.drainSteps_eq line 122
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.additionTraceAt line 128
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.traceAt line 153
  34. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerCleanup.executionAt line 173