OAI/Computability/DirectedFeedback/Machines/RawInitialMachineStart.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.inputTapes line 55
2. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.firstTapes_inline_RawInitialMachineStart line 59
3. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.counterTapes line 64
4. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.headerTapes_inline_RawInitialMachineStart line 70
5. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.startTapes line 77
6. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.initList_eq line 85
7. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.trace_trans_inline_RawInitialMachineStart line 94
8. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.readCountersTrace line 98
9. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.headersTrace line 132
10. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.initializeIndexTrace line 151
11. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.startTrace line 163
12. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.formulaStartTrace line 173
13. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.startInTime line 183
14. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineStart.formulaStartInTime line 192
15. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput line 212
16. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput_nil line 215
17. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput_cons line 217
18. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput line 221
19. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoopData.mapIdx_ofFn_inline_RawInitialMachineLoopData line 225
20. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_nil line 231
21. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_cons line 233
22. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_numbered line 240
23. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoopData.tableWords_decomposition line 250
24. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoopData.loopTapes line 257
25. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoopData.startTapes_eq line 265
26. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoopData.decrement_counter line 271
27. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineLoopData.increment_index line 277
28. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachinePhases.copySource_ne_scratch line 292
29. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachinePhases.copySource_ne_reversed line 295
30. def OAI.DFVSGames.Foundations.PCP.RawInitialMachinePhases.copyInTime line 298
31. def OAI.DFVSGames.Foundations.PCP.RawInitialMachinePhases.relationInTime line 313
32. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachinePhases.bitWord_head_inline_RawInitialMachinePhases line 326
33. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachinePhases.loadSigns_step line 330
34. def OAI.DFVSGames.Foundations.PCP.RawInitialMachinePhases.loadSignsInTime line 339
35. def OAI.DFVSGames.Foundations.PCP.RawInitialMachinePhases.cleanupFieldInTime line 350
36. def OAI.DFVSGames.Foundations.PCP.RawInitialMachinePhases.cleanupFinalInTime line 358
37. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineReadClause.fieldValue line 375
38. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes line 380
39. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes_input line 386
40. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes_field line 390
41. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes_other line 394
42. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineReadClause.recordTapes_name line 402
43. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineReadClause.trace_trans_inline_RawInitialMachineReadClause line 408
44. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineReadClause.fieldsTrace line 412
45. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineReadClause.readClauseTrace line 508
46. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineReadClause.readClauseInTime line 528
47. abbrev OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.advance_inline_RawInitialMachineRows line 553
48. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.outputTapes line 555
49. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.outputTapes_reversed line 558
50. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.outputTapes_other line 561
51. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.outputTapes_twice line 565
52. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.trace_trans_inline_RawInitialMachineRows line 572
53. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.copyTrace_inline_RawInitialMachineRows line 576
54. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.closeTailTrace_inline_RawInitialMachineRows line 584
55. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.closeReverseTrace_inline_RawInitialMachineRows line 592
56. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.reverse_encodeWord_add_inline_RawInitialMachineRows line 602
57. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.rowEndBits line 608
58. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.rowEndTrace_inline_RawInitialMachineRows line 612
59. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.rowEndBits_append_inline_RawInitialMachineRows line 644
60. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.falseRowTrace line 653
61. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.trueRowTrace line 691
62. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.pairWords line 720
63. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.pairTrace line 725
64. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.rowsTrace line 751
65. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineRows.rowsInTime line 798
66. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineCleanup.trace_trans_inline_RawInitialMachineCleanup line 824
67. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineCleanup.incrementIndexTrace line 828
68. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineCleanup.cleanupTrace line 834
69. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineCleanup.cleanupInTime line 917