OAI/Combinatorics/IndependentSets/Machines/MachineLogCounter.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.bitLength line 13
  2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.bitLength_zero line 15
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.bitLength_positive line 17
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.bitLength_half line 20
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.increments line 27
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.increments_true line 30
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.increments_half line 33
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.increments_false line 37
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.coreTime line 42
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.coreTime_zero line 47
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.coreTime_positive line 49
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.coreTime_bound line 53
  13. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.Alphabet line 63
  14. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.State line 64
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.initialState line 66
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.rawTapes line 68
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.update_input line 73
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.update_scratch line 78
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.update_output line 83
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.stripLoop line 88
  21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.guardLoop line 94
  22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.halfLoop line 103
  23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.program line 112
  24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.machine line 119
  25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.configuration line 130
  26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.next line 134
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.stripStep_true line 136
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.stripStep_false line 144
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.stripTrace line 152
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.halfStep_nil line 168
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.halfStep_false line 176
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.halfStep_true line 185
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.halfTrace line 194
  34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.restoreTrace line 226
  35. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.guardStep_zero line 243
  36. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.guardStep_positive line 252
  37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.coreTrace line 264
  38. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.initList_eq line 300
  39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.haltList_eq line 308
  40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.initialStep line 316
  41. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.totalTime line 325
  42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.totalTime_bound line 327
  43. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.machineTrace line 332
  44. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.outputsInTime line 347
  45. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLogCounter.computableInPolyTime line 353