OAI/MathematicalPhysics/RapidForcing/MachineRun.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RapidForcing.radix line 9
2. lemma OAI.RapidForcing.radix_lt line 12
3. lemma OAI.RapidForcing.radix_digit line 23
4. lemma OAI.RapidForcing.radix_update line 47
5. lemma OAI.RapidForcing.radix_eq_ofDigits line 63
6. lemma OAI.RapidForcing.radix_expand line 76
7. def OAI.RapidForcing.Machine.ValidAt line 86
8. def OAI.RapidForcing.Machine.tapeCode line 90
9. def OAI.RapidForcing.Machine.configCode line 94
10. lemma OAI.RapidForcing.Machine.initialConfig_valid line 98
11. lemma OAI.RapidForcing.Machine.nextConfig_head_bounds line 107
12. lemma OAI.RapidForcing.Machine.nextConfig_tape_of_ne line 119
13. lemma OAI.RapidForcing.Machine.nextConfig_preserves_blanks line 128
14. lemma OAI.RapidForcing.Machine.nextConfig_valid line 134
15. lemma OAI.RapidForcing.Machine.run_succ line 143
16. lemma OAI.RapidForcing.Machine.run_valid line 146
17. lemma OAI.RapidForcing.Machine.headIndex_bounds line 151
18. lemma OAI.RapidForcing.Machine.tapeCode_lt line 159
19. lemma OAI.RapidForcing.Machine.configCode_lt line 165
20. lemma OAI.RapidForcing.Machine.configCode_read line 175
21. lemma OAI.RapidForcing.Machine.tapeCode_read line 197
22. lemma OAI.RapidForcing.Machine.nextConfig_instruction line 207
23. lemma OAI.RapidForcing.Machine.tapeCode_extend line 225
24. lemma OAI.RapidForcing.Machine.tapeCode_next line 242
25. theorem OAI.RapidForcing.Machine.nextDigit_configCode line 268
26. lemma OAI.RapidForcing.Machine.terminalDigit_configCode line 288
27. lemma OAI.RapidForcing.Machine.initialConfig_tape_val line 295
28. lemma OAI.RapidForcing.Machine.configCode_initial line 303
29. def OAI.RapidForcing.Machine.runCode line 318
30. lemma OAI.RapidForcing.Machine.runCode_lt line 320
31. lemma OAI.RapidForcing.Machine.runCode_zero line 323
32. lemma OAI.RapidForcing.Machine.runCode_succ line 326
33. lemma OAI.RapidForcing.Machine.runCode_terminal line 332