OAI/Computability/MinUncut/Machines/MachineFiniteSequence.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Complexity.MachineFiniteSequence.Label line 12
  2. instance OAI.MinUncutGames.Foundations.Complexity.MachineFiniteSequence.labelFintype line 16
  3. instance OAI.MinUncutGames.Foundations.Complexity.MachineFiniteSequence.labelDecidableEq line 24
  4. def OAI.MinUncutGames.Foundations.Complexity.MachineFiniteSequence.entry line 35
  5. def OAI.MinUncutGames.Foundations.Complexity.MachineFiniteSequence.instruction line 42
  6. def OAI.MinUncutGames.Foundations.Complexity.MachineFiniteSequence.resultOf line 53
  7. def OAI.MinUncutGames.Foundations.Complexity.MachineFiniteSequence.steps line 57
  8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFiniteSequence.trace line 63
  9. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.Alphabet line 109
  10. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.Tapes line 110
  11. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.LocalLabel line 111
  12. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.Label line 112
  13. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.Data line 113
  14. def OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.entry line 115
  15. def OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.localInstruction line 118
  16. def OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.instruction line 122
  17. def OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.result line 127
  18. def OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.cost line 130
  19. def OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.finalTapes line 132
  20. def OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.finalRegister line 136
  21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.finalRegister_none line 141
  22. def OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.steps line 144
  23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.sequence_result line 149
  24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.sequence_steps line 159
  25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.finalTapes_apply line 166
  26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.finalTapes_mem line 177
  27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.finalTapes_not_mem line 180
  28. def OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.lengthSum line 183
  29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.lengthSum_mono line 187
  30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.steps_le line 196
  31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.steps_le_uniform line 212
  32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.trace line 227
  33. def OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.execution line 248
  34. def OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.workTapes line 260
  35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.mem_workTapes line 263
  36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.workTapes_length_le line 270
  37. def OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.haltTapes line 275
  38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.finalTapes_workTapes line 278
  39. theorem OAI.MinUncutGames.Foundations.Complexity.MachineDrainMany.cleanupTrace line 288