OAI/Combinatorics/IndependentSets/Machines/MachineRepeat.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.ExtraTape line 12
  2. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.(instance at line 15) line 15
  3. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.Phase line 19
  4. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.(instance at line 22) line 22
  5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.Tape line 26
  6. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.Symbols line 27
  7. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.Label line 28
  8. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.State line 29
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.extraTapes line 31
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.auxProgram line 37
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.program line 58
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.machine line 62
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.inputTapes line 80
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.inputTapes_input line 83
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.inputTapes_counter line 87
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.inputConfig line 90
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.embedded line 94
  18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.temporaryTapes line 99
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.temporaryConfig line 102
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.inputTapes_update_input line 106
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.inputTapes_update_counter line 118
  22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.oneStep line 127
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.parseStep_true line 135
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.parseStep_false line 144
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.parseTrace line 153
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.guardStep_some line 180
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.guardStep_none line 189
  28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.bodyExecution line 196
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.bodyToTemp_tapes line 206
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.tempToBody_tapes line 222
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.finalToTemp_tapes line 234
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.tempToOutput_tapes line 246
  33. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.bodyToTemp line 258
  34. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.tempToBody line 274
  35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.finalToTemp line 289
  36. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.tempToOutput line 301
  37. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.bodyReturn line 314
  38. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.finish line 325
  39. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.loopBudget line 337
  40. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.loopExecution line 342
  41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.inputConfig_init line 382
  42. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.executeSequence line 394
  43. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.loopBudget_eq_sum line 425
  44. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.executeSequenceSum line 436
  45. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRepeat.loopBudget_le line 449