OAI/Computability/BinPacking/Reductions/MachineSubstitution.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Reduction.MachineSubstitution.pushWord line 15
  2. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.stepAux_pushWord line 20
  3. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.statementPushBound_pushWord line 34
  4. def OAI.BinPackingGames.Reduction.MachineSubstitution.loop line 46
  5. def OAI.BinPackingGames.Reduction.MachineSubstitution.program line 52
  6. def OAI.BinPackingGames.Reduction.MachineSubstitution.machine line 57
  7. def OAI.BinPackingGames.Reduction.MachineSubstitution.maxEmission line 68
  8. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.statementPushBound_le line 71
  9. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.programPushBound_le line 81
  10. def OAI.BinPackingGames.Reduction.MachineSubstitution.tapeStacks line 91
  11. def OAI.BinPackingGames.Reduction.MachineSubstitution.running line 94
  12. def OAI.BinPackingGames.Reduction.MachineSubstitution.emitting line 98
  13. def OAI.BinPackingGames.Reduction.MachineSubstitution.halted line 102
  14. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.update_input line 105
  15. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.update_output line 110
  16. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.step_empty line 115
  17. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.step_cons line 122
  18. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.step_emit line 131
  19. def OAI.BinPackingGames.Reduction.MachineSubstitution.next line 145
  20. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.two_steps_cons line 149
  21. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.substitution_steps line 158
  22. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.initList_eq line 173
  23. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.haltList_eq line 180
  24. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.substitution_init_steps line 185
  25. def OAI.BinPackingGames.Reduction.MachineSubstitution.outputsInTime line 191
  26. theorem OAI.BinPackingGames.Reduction.MachineSubstitution.outputsInTime_steps line 198
  27. def OAI.BinPackingGames.Reduction.MachineSubstitution.computableInPolyTime line 201