OAI/Combinatorics/IndependentSets/Machines/MachineFiniteSequence.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteSequence.Label line 13
  2. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteSequence.labelFintype line 17
  3. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteSequence.labelDecidableEq line 25
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteSequence.entry line 36
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteSequence.instruction line 43
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteSequence.resultOf line 54
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteSequence.steps line 58
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteSequence.trace line 64
  9. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.Command line 109
  10. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.LocalLabel line 110
  11. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.Label line 111
  12. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.entry line 113
  13. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.instruction line 117
  14. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.result line 124
  15. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.finalTapes line 128
  16. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.steps line 132
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.planTrace line 137
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.ready_finalTapes line 163
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.finalTapes_output line 176
  20. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan line 197
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan_values line 204
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachinePlan.rowPlan_output line 209