OAI/Combinatorics/IndependentSets/Machines/MachineUnaryLess.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.Alphabet line 12
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.State line 13
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.zeroTest line 15
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.zeroTestTrace line 21
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.tapes line 36
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.tapes_left line 41
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.tapes_right line 46
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.tapes_savedLeft line 51
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.tapes_savedRight line 56
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.update_tapes line 61
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.tapes_self line 79
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.stop line 83
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.scan line 87
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_zero_left line 102
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_zero_right line 115
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_succ line 128
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.scanTrace line 143
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.transferLeft_tapes line 174
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.transferRight_tapes line 181
  20. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.Label line 188
  21. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.(instance at line 194) line 194
  22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.statement line 198
  23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.steps line 206
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.comparisonTrace line 208
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.lessThanTrace line 261
  26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.timePolynomial line 279
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.steps_le_time line 281
  28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.lessThanInPolynomialTime line 287
  29. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.machine line 303
  30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryLessAt.machineInPolynomialTime line 314