OAI/Combinatorics/IndependentSets/Machines/MachineControl.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineControl.configuration line 13
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineControl.statement line 19
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineControl.stepAux_simulation line 34
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineControl.program line 61
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineControl.step_simulation line 64
  6. inductive OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.Tape line 84
  7. instance OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.(instance at line 90) line 90
  8. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.Alphabet line 96
  9. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.Flags line 98
  10. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.Ambient line 99
  11. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.State line 100
  12. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.normal line 102
  13. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.initial line 105
  14. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.context line 107
  15. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareEquiv line 110
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareEquiv_normal line 117
  17. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.emitterEquiv line 122
  18. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.setupPorts line 128
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.setupPorts_injective line 131
  20. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.headPorts line 135
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.headPorts_injective line 138
  22. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.rowSources line 142
  23. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.headerSources line 143
  24. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.fieldPorts line 144
  25. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts line 146
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts_ne_output line 150
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.cleanupPorts_cover line 153
  28. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.compareStatement line 175
  29. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.emitterStatement line 180
  30. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.storeLoop line 184
  31. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.stepAux_storeLoop line 187
  32. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.nextRow line 192
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.stepAux_nextRow line 196
  34. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.RuntimeModel.transportInTime line 204