OAI/GroupTheory/UniversalGroup/TuringMachines.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Higman.MicroTM2.Stmt line 11
2. abbrev OAI.Higman.MicroTM2.Cfg line 12
3. def OAI.Higman.MicroTM2.step line 16
4. def OAI.Higman.MicroTM2.translate line 27
5. def OAI.Higman.MicroTM2.project line 30
6. theorem OAI.Higman.MicroTM2.reaches_stepAux line 34
7. theorem OAI.Higman.MicroTM2.translate_step line 54
8. theorem OAI.Higman.MicroTM2.translate_reaches line 62
9. theorem OAI.Higman.MicroTM2.project_step line 68
10. theorem OAI.Higman.MicroTM2.project_reaches line 102
11. theorem OAI.Higman.MicroTM2.reaches_project_translate line 108
12. theorem OAI.Higman.MicroTM2.reaches_halt_iff line 114
13. def OAI.Higman.TM2StackCompiler.readOp line 128
14. lemma OAI.Higman.TM2StackCompiler.readOp_rel line 132
15. lemma OAI.Higman.TM2StackCompiler.readAction_rel line 136
16. def OAI.Higman.TM2StackCompiler.rawAction line 148
17. def OAI.Higman.TM2StackCompiler.rawTarget line 155
18. lemma OAI.Higman.TM2StackCompiler.raw_sound line 168
19. lemma OAI.Higman.TM2StackCompiler.raw_complete line 186
20. lemma OAI.Higman.TM2StackCompiler.target_mem line 224
21. abbrev OAI.Higman.TM2StackCompiler.State line 244
22. abbrev OAI.Higman.TM2StackCompiler.Edge line 245
23. instance OAI.Higman.TM2StackCompiler.(instance at line 247) line 247
24. instance OAI.Higman.TM2StackCompiler.(instance at line 248) line 248
25. def OAI.Higman.TM2StackCompiler.compile line 256
26. def OAI.Higman.TM2StackCompiler.forget line 263
27. lemma OAI.Higman.TM2StackCompiler.compile_sound line 266
28. lemma OAI.Higman.TM2StackCompiler.compile_complete line 272
29. lemma OAI.Higman.TM2StackCompiler.run_sound line 284
30. lemma OAI.Higman.TM2StackCompiler.reaches_complete line 292
31. lemma OAI.Higman.TM2StackCompiler.weights_one line 305