OAI/Combinatorics/IndependentSets/Machines/MachineRegularDummyRow.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.Tape line 12
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.Alphabet line 13
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.State line 14
  4. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.Label line 16
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.reverseIndex line 22
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.emittedBits line 24
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.instruction line 27
  8. structure OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.Input line 40
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.memory line 47
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.memory_input line 50
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.join_trace line 53
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.affine_frame line 57
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.cleanup_frame line 65
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.rowTraceAt line 74
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.cleanupTraceAt line 96
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.steps line 121
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.timeBound line 126
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.steps_eq line 129
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.traceAt line 135
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.machine line 162
  21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularDummyRow.machineInTime line 173