OAI/Combinatorics/IndependentSets/Machines/MachineUnaryAdd.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.Alphabet line 16
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.finish line 18
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.loop line 22
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.loopPushBound line 32
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes line 36
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_source line 41
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_destination line 47
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_other line 53
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.update_source line 60
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.update_destination line 73
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_true line 83
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_false line 92
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_succ line 100
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_zero line 111
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.step_succ line 123
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.step_zero line 137
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.addTrace line 151
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.addFromTapes line 175
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.addInTime line 195
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAddAt.addInTime_steps line 213