OAI/Combinatorics/IndependentSets/Machines/MachineStateEquiv.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.statement line 13
  2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.statement_symm_statement line 16
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.configuration line 22
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.configuration_label line 25
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.configuration_state line 28
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.configuration_tapes line 31
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.configuration_symm_configuration line 34
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.configuration_configuration_symm line 39
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.configurationEquiv line 44
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.configurationEquiv_apply line 50
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.control_configuration line 53
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.program line 58
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.program_symm_program line 61
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.statementPushBound line 66
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.supportsStmt_iff line 71
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.supports_iff line 93
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.stepAux_transport line 99
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.stepAux_transport_symm line 106
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.step_transport line 113
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.step_iff line 125
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.advance_transport line 137
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.iterate_transport line 145
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.trace_iff line 156
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.trace line 172
  25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.execution line 179
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.execution_steps line 193
  27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.execution_reflect line 198
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateEquiv.execution_reflect_steps line 213