OAI/Combinatorics/IndependentSets/Machines/PoweringMachineVertex.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.Command line 13
  2. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.ports line 15
  3. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.direction line 18
  4. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.commands line 21
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.commands_length line 23
  6. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.LocalLabel line 27
  7. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.SequenceLabel line 28
  8. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.Label line 29
  9. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.State line 30
  10. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.sequenceEntry line 32
  11. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.entry line 37
  12. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.sequenceInstruction line 40
  13. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.instruction line 49
  14. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.result line 55
  15. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes line 61
  16. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.finalTapes line 67
  17. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.sequenceSteps line 72
  18. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.costSum line 78
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.sequenceSteps_eq line 84
  20. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.steps line 97
  21. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.budget line 100
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.costSum_le line 103
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.steps_le line 116
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.sequenceTrace line 120
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.vertexTrace line 150
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_ready line 168
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_ready line 182
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_other line 191
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_other line 205
  30. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.rowBits line 212
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.blockIndex_eq_encodeDart line 216
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.rowBits_eq line 224
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.encodeWords_flatMap line 231
  34. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.rows_eq_vertexRowBits line 237
  35. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_output line 263
  36. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_output line 283
  37. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineVertex.vertexInTime line 294