OAI/Computability/MinUncut/PCP/ContextPrepare.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.Arena line 13
2. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.LoadState line 14
3. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.PrepareState line 15
4. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.State line 16
5. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.Label line 17
6. def OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.prepareEntry line 21
7. def OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.stateSwap line 25
8. def OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.program line 28
9. def OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.preparationConfiguration line 34
10. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.preparation_step line 42
11. def OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.initialState line 61
12. def OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.finalState line 65
13. def OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.loadInTime line 70
14. def OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.signatureInTime line 91
15. def OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.prepareInTime line 113
16. def OAI.MinUncutGames.Foundations.Hastad.SourceContextPrepare.machine line 135
17. inductive OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.HeaderTape line 158
18. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.HeaderTape.enumList line 162
19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.HeaderTape.enumList_getElem?_ctorIdx_eq line 164
20. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.HeaderTape.enumList_nodup line 168
21. instance OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.(instance at line 170) line 170
22. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.Tape line 174
23. inductive OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.Label line 176
24. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.variableHeader line 184
25. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.clauseHeader line 185
26. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.headerDestination line 186
27. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.readStart line 187
28. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.readLoop line 188
29. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.labelAt line 189
30. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.program line 191
31. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.atReadStart line 210
32. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.atReadLoop line 215
33. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.atReadDone line 220
34. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.copiedInput line 226
35. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.readOutput line 229
36. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.headerOutput line 233
37. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.clear_readOutput line 238
38. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.readOutput_work line 248
39. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.headerOutput_frame line 253
40. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.headerInTime line 257
41. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.digitOutput line 293
42. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.digitOutput_frame line 296
43. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.digitInTime line 300
44. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.stageTapes line 343
45. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.stageTapes_frame line 348
46. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.stageTapes_current line 359
47. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.stageTapes_remaining line 379
48. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.prefixInTime line 400
49. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.digitsInTime line 428
50. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.outputTapes line 447
51. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.initializeInTime line 450
52. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.output_current line 482
53. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.output_remaining line 486
54. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.output_frame line 490
55. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.output_work line 496
56. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.output_variableHeader line 501
57. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.output_clauseHeader line 506
58. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.output_headers line 511
59. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.output_formula line 517
60. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.timePolynomial line 522
61. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.timePolynomial_eval line 525
62. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopInit.machine line 529