OAI/Combinatorics/IndependentSets/Machines/MachineTransfer.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Reduction.MachineTransfer.alphabet line 10
  2. def OAI.IndependentSetsGames.Reduction.MachineTransfer.loop line 16
  3. def OAI.IndependentSetsGames.Reduction.MachineTransfer.machine line 23
  4. def OAI.IndependentSetsGames.Reduction.MachineTransfer.tapeStacks line 35
  5. def OAI.IndependentSetsGames.Reduction.MachineTransfer.running line 40
  6. def OAI.IndependentSetsGames.Reduction.MachineTransfer.halted line 44
  7. theorem OAI.IndependentSetsGames.Reduction.MachineTransfer.update_input line 48
  8. theorem OAI.IndependentSetsGames.Reduction.MachineTransfer.update_output line 54
  9. theorem OAI.IndependentSetsGames.Reduction.MachineTransfer.step_empty line 59
  10. theorem OAI.IndependentSetsGames.Reduction.MachineTransfer.step_cons line 67
  11. def OAI.IndependentSetsGames.Reduction.MachineTransfer.next line 76
  12. theorem OAI.IndependentSetsGames.Reduction.MachineTransfer.transfer_steps line 79
  13. theorem OAI.IndependentSetsGames.Reduction.MachineTransfer.initList_eq line 96
  14. theorem OAI.IndependentSetsGames.Reduction.MachineTransfer.haltList_eq line 103
  15. theorem OAI.IndependentSetsGames.Reduction.MachineTransfer.transfer_init_steps line 110
  16. def OAI.IndependentSetsGames.Reduction.MachineTransfer.outputsInTime line 117
  17. theorem OAI.IndependentSetsGames.Reduction.MachineTransfer.outputsInTime_steps line 124
  18. def OAI.IndependentSetsGames.Reduction.MachineTransfer.computableInPolyTime line 127