OAI/Combinatorics/IndependentSets/Machines/MachineAlphabetTransport.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.tapes line 12
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.statement line 14
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.configuration line 16
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.program line 18
5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.castStatement line 21
6. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.castConfiguration line 22
7. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.castProgram line 23
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.tapes_rfl line 25
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.statement_rfl line 26
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.configuration_rfl line 27
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.program_rfl line 28
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.program_apply line 30
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.statement_roundtrip line 33
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.statement_symm_roundtrip line 36
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.configuration_roundtrip line 39
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.configuration_symm_roundtrip line 42
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.program_roundtrip line 45
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.program_symm_roundtrip line 48
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.tapes_roundtrip line 51
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.tapes_symm_roundtrip line 54
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.configuration_label line 57
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.configuration_state line 60
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.configuration_tapes line 63
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.configuration_mk line 66
25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.map_configuration_rfl line 70
26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.stepAux_simulation line 75
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.step_simulation line 80
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.trace_transport line 86
29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.successfulTrace line 94
30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.executionInTime line 102
31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.executionInTime_steps line 114
32. def OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.successfulExecutionInTime line 119
33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineAlphabetTransport.successfulExecutionInTime_steps line 125