OAI/Combinatorics/IndependentSets/Machines/MachineReverse.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Reduction.MachineReverse.loop line 11
  2. def OAI.IndependentSetsGames.Reduction.MachineReverse.machine line 17
  3. def OAI.IndependentSetsGames.Reduction.MachineReverse.tapeStacks line 28
  4. def OAI.IndependentSetsGames.Reduction.MachineReverse.running line 31
  5. def OAI.IndependentSetsGames.Reduction.MachineReverse.halted line 34
  6. theorem OAI.IndependentSetsGames.Reduction.MachineReverse.update_input line 37
  7. theorem OAI.IndependentSetsGames.Reduction.MachineReverse.update_output line 42
  8. theorem OAI.IndependentSetsGames.Reduction.MachineReverse.step_empty line 47
  9. theorem OAI.IndependentSetsGames.Reduction.MachineReverse.step_cons line 54
  10. def OAI.IndependentSetsGames.Reduction.MachineReverse.next line 62
  11. theorem OAI.IndependentSetsGames.Reduction.MachineReverse.reverse_steps line 65
  12. theorem OAI.IndependentSetsGames.Reduction.MachineReverse.initList_eq line 79
  13. theorem OAI.IndependentSetsGames.Reduction.MachineReverse.haltList_eq line 86
  14. theorem OAI.IndependentSetsGames.Reduction.MachineReverse.reverse_init_steps line 90
  15. def OAI.IndependentSetsGames.Reduction.MachineReverse.outputsInTime line 96
  16. theorem OAI.IndependentSetsGames.Reduction.MachineReverse.outputsInTime_steps line 102
  17. def OAI.IndependentSetsGames.Reduction.MachineReverse.computableInPolyTime line 105
  18. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.Alphabet line 128
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.tapes line 131
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.tapes_first line 137
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.tapes_second line 139
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.tapes_third line 141
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.tapes_involutive line 144
  24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.configuration line 149
  25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.statement line 155
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.tapes_update_first line 172
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.tapes_update_second line 184
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.tapes_update_third line 196
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.stepAux_simulation line 208
  30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.program line 256
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStackSwap.step_simulation line 259