OAI/Combinatorics/IndependentSets/Machines/PushWord.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Reduction.MachineSubstitution.pushWord line 17
  2. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.stepAux_pushWord line 22
  3. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.statementPushBound_pushWord line 36
  4. def OAI.IndependentSetsGames.Reduction.MachineSubstitution.loop line 48
  5. def OAI.IndependentSetsGames.Reduction.MachineSubstitution.program line 54
  6. def OAI.IndependentSetsGames.Reduction.MachineSubstitution.machine line 59
  7. def OAI.IndependentSetsGames.Reduction.MachineSubstitution.maxEmission line 70
  8. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.statementPushBound_le line 73
  9. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.programPushBound_le line 83
  10. def OAI.IndependentSetsGames.Reduction.MachineSubstitution.tapeStacks line 93
  11. def OAI.IndependentSetsGames.Reduction.MachineSubstitution.running line 96
  12. def OAI.IndependentSetsGames.Reduction.MachineSubstitution.emitting line 100
  13. def OAI.IndependentSetsGames.Reduction.MachineSubstitution.halted line 104
  14. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.update_input line 107
  15. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.update_output line 112
  16. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.step_empty line 117
  17. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.step_cons line 124
  18. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.step_emit line 133
  19. def OAI.IndependentSetsGames.Reduction.MachineSubstitution.next line 147
  20. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.two_steps_cons line 151
  21. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.substitution_steps line 160
  22. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.initList_eq line 175
  23. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.haltList_eq line 182
  24. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.substitution_init_steps line 187
  25. def OAI.IndependentSetsGames.Reduction.MachineSubstitution.outputsInTime line 193
  26. theorem OAI.IndependentSetsGames.Reduction.MachineSubstitution.outputsInTime_steps line 200
  27. def OAI.IndependentSetsGames.Reduction.MachineSubstitution.computableInPolyTime line 203