OAI/Combinatorics/IndependentSets/Machines/HeaderStates.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.headerStates line 13
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.readyState line 21
  3. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase line 23
  4. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.(instance at line 26) line 26
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.copySource line 30
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.copyTarget line 33
  7. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.Label line 37
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.copyExit line 52
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.clearTape line 56
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.clearEntry line 60
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.program line 63
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.machine line 83
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.frame line 94
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.cfg line 100
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.frame_core line 105
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.bodyPlacement line 109
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.headerAux line 118
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.headerAux_empty line 124
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.headerPlacement line 128
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.inputData line 155
  21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.headerData line 168
  22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.headerStacks line 171
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.headerTrace line 175
  24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.oldData line 194
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.originalData_eq line 197
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.oldBodyTrace line 200
  27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.counterStacks line 215
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.frame_oldFuel line 218
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.frame_ownerFuel line 222
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_oldFuel line 226
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_ownerFuel line 237
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_global line 248
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_owner line 261
  34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.oldGuardStep line 274
  35. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.oldGuardExit line 288
  36. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.oldIncrementStep line 299
  37. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.oldPrefix line 313
  38. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed line 316
  39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.joinTrace line 323
  40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.oldPrefixTrace line 327
  41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.oldLoopTrace line 358
  42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.frame_scratch line 370
  43. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.frame_darts line 374
  44. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.frame_header_n line 377
  45. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.oldSeedStep line 381
  46. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.copyOldTrace line 394
  47. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.oldStageTrace line 409
  48. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_offset line 419