OAI/Computability/FourierTransform/ProgramConstruction.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PowerSaving.RAM.Can.unfold_bound line 16
2. theorem OAI.PowerSaving.RAM.Can.reindex line 23
3. theorem OAI.PowerSaving.RAM.Can.cong line 28
4. theorem OAI.PowerSaving.RAM.Can.weaken line 32
5. theorem OAI.PowerSaving.RAM.Can.mono line 36
6. theorem OAI.PowerSaving.RAM.Can.ambient line 40
7. theorem OAI.PowerSaving.RAM.Can.pipe line 44
8. theorem OAI.PowerSaving.RAM.Can.then_do line 48
9. theorem OAI.PowerSaving.RAM.Can.fork line 52
10. theorem OAI.PowerSaving.RAM.Can.pair line 56
11. theorem OAI.PowerSaving.RAM.Can.save line 60
12. theorem OAI.PowerSaving.RAM.Can.bind line 64
13. theorem OAI.PowerSaving.RAM.Can.id line 68
14. theorem OAI.PowerSaving.RAM.Can.first line 70
15. theorem OAI.PowerSaving.RAM.Can.second line 73
16. theorem OAI.PowerSaving.RAM.Can.fst line 76
17. theorem OAI.PowerSaving.RAM.Can.snd line 79
18. theorem OAI.PowerSaving.RAM.Can.wc line 82
19. theorem OAI.PowerSaving.RAM.Can.zero line 86
20. theorem OAI.PowerSaving.RAM.Can.one line 89
21. theorem OAI.PowerSaving.RAM.Can.add line 94
22. theorem OAI.PowerSaving.RAM.Can.sub line 98
23. theorem OAI.PowerSaving.RAM.Can.mul line 102
24. theorem OAI.PowerSaving.RAM.Can.cross line 106
25. theorem OAI.PowerSaving.RAM.Can.inv line 111
26. theorem OAI.PowerSaving.RAM.Can.look line 118
27. theorem OAI.PowerSaving.RAM.Can.len line 122
28. theorem OAI.PowerSaving.RAM.Can.nop line 127
29. theorem OAI.PowerSaving.RAM.Can.wadd line 139
30. theorem OAI.PowerSaving.RAM.Can.wsub line 144
31. theorem OAI.PowerSaving.RAM.Can.wmul line 149
32. theorem OAI.PowerSaving.RAM.Can.wdiv line 154
33. theorem OAI.PowerSaving.RAM.Can.wmod line 159
34. theorem OAI.PowerSaving.RAM.Can.wlt line 164
35. theorem OAI.PowerSaving.RAM.Can.testz line 168
36. theorem OAI.PowerSaving.RAM.Can.loop line 180
37. theorem OAI.PowerSaving.RAM.Can.tab line 191
38. theorem OAI.PowerSaving.RAM.Can.sow line 201