OAI/Combinatorics/IndependentSets/Machines/ComputeTime.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.prefixTrace line 14
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.computeTime line 34
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.computeTrace line 37
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.headerBits line 75
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.headerBits_eq line 78
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.headerBits_length line 82
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.cleanupZerosStep line 88
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.emitTime line 97
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.emitTrace line 101
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.totalTime line 164
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.trace line 167
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.arithmeticPolynomial line 180
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.timePolynomial line 187
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.totalTime_le line 190
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.inTime line 232
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Fuel.guard line 252
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Fuel.guard_succ line 260
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Fuel.guard_zero line 267
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Fuel.increment line 274
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Fuel.increment_step line 277
  21. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.Body line 287
  22. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.Tape line 288
  23. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.Alphabet line 289
  24. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.State line 290
  25. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.Data line 291
  26. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.BaseTable line 292
  27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.sumDecidableEq line 294
  28. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.tapeDecidableEq line 305
  29. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.tapeBEq line 320
  30. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.tapeLawfulBEq line 323
  31. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.tapeFintype line 327
  32. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.coreTape line 335
  33. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.oldFuel line 336
  34. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerFuel line 337
  35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.dummyFuel line 338
  36. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.scratch line 339
  37. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.headerTape line 341
  38. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.headerView line 347
  39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.headerView_left line 358
  40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.headerView_right line 367
  41. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.bodyView line 386
  42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.bodyView_left line 390
  43. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.bodyView_right line 391
  44. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerTape line 397
  45. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerView line 401
  46. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerView_left line 409
  47. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerView_right line 415