OAI/Combinatorics/IndependentSets/Machines/MachineFiniteTable.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteTable.dispatch line 16
  2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteTable.stepAux_dispatch line 23
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteTable.dispatch_push_bound line 41
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteTable.emit line 53
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteTable.tableBound line 57
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteTable.stepAux_emit line 60
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteTable.emit_push_bound line 67
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteTable.emitInTime line 73
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFiniteTable.output_frame line 90
  10. inductive OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.Tape line 101
  11. abbrev OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.Signs line 108
  12. abbrev OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.State line 109
  13. abbrev OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.Alphabet line 110
  14. inductive OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.CopyPhase line 112
  15. inductive OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.Label line 122
  16. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.initialState line 138
  17. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.stateKeys line 140
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.stateKeys_complete line 145
  19. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.nameField line 151
  20. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.copySource line 153
  21. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.copyScale line 158
  22. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.copyNext line 162
  23. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.relationNext line 171
  24. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.finalTape line 177
  25. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.drain line 180
  26. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.headerTape line 183
  27. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.relationOutput line 185
  28. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.program line 189
  29. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineModel.machine line 239