OAI/Computability/MinUncut/PCP/ContextLoad.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.Tape line 12
2. inductive OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.Label line 19
3. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.place line 28
4. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.fill line 32
5. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.fill_place line 39
6. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.fill_self line 44
7. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.fill_update line 54
8. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.placedLabel line 63
9. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.placedConfiguration line 67
10. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.placedStatement line 73
11. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.placed_stepAux line 85
12. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.nextLabel line 110
13. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.program line 113
14. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.placed_step line 124
15. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.lookupOutput line 141
16. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.placedLookupInTime line 146
17. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.copiedTapes line 162
18. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.coordinateOutput line 165
19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.cleanup_lookupOutput line 173
20. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_current line 202
21. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_remaining line 207
22. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_field line 212
23. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.coordinateOutput_other_field line 219
24. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.suffix_length_le_input line 224
25. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.coordinateInTime line 236
26. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.labelAt line 281
27. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.nextLabel_eq line 284
28. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.stageTapes line 286
29. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.stageTapes_frame line 294
30. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.stageTapes_clean line 307
31. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.stageTapes_field line 319
32. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.prefixInTime line 344
33. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.loadInTime line 387
34. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.clauses_length_le_input line 410
35. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.loadUnaryInTime line 415
36. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.timePolynomial line 438
37. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.timePolynomial_eval line 441
38. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.variableSlot line 447
39. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.polaritySlot line 448
40. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.variableField line 449
41. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.polarityField line 450
42. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.clauseWords_variable line 452
43. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.clauseWords_polarity line 458
44. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.output_variable line 466
45. theorem OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.output_polarity line 473
46. def OAI.MinUncutGames.Foundations.Hastad.SourceContextLoad.machine line 482
47. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.Position line 499
48. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.NameProfile line 500
49. structure OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.Signature line 502
50. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.signatureEquiv line 508
51. instance OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.signatureFintype line 515
52. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.card_position line 519
53. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.card_signature line 522
54. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.positiveAt line 528
55. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.occurrenceName line 533
56. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.contextNameProfile line 537
57. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.ofContext line 540
58. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.ofContext_signs line 546
59. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.ofContext_sameName line 550
60. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.ofContext_selected line 555
61. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.signatureSatisfies line 558
62. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.signatureValid line 563
63. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.signatureSatisfies_ofContext line 568
64. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.signature_validJ line 573
65. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.signatureCanonicalSlot line 596
66. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.signatureProjection line 600
67. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.signatureCanonicalSlot_ofContext line 603
68. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.signature_pi line 618
69. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.signature_projection_selected line 624
70. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.validJ_eq_of_signature_eq line 633
71. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalSignature.pi_eq_of_signature_eq line 639
72. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.LocalKey line 653
73. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.LocalInput line 654
74. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.signatureEncoding line 656
75. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.signatureList line 662
76. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.mem_signatureList line 664
77. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.signatureList_nodup line 667
78. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.signatureList_length line 670
79. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.localInputEncoding line 674
80. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.localInputs line 677
81. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.mem_localInputs line 679
82. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.localInputs_nodup line 682
83. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.localInputs_length line 685
84. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.localKeyEncoding line 689
85. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.emptyLocalAddress line 693
86. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.foldedLocalAddress line 697
87. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.equationFor line 703
88. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.equation line 711
89. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.emit line 715
90. def OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.addressMap line 718
91. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.mapEquation_comp line 724
92. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.addressMap_emptyLocalAddress line 727
93. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.addressMap_foldedLocalAddress line 733
94. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.contextEquation_eq_map_equationFor line 742
95. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.contextEquation_eq_map line 755
96. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLocalEquation.sourceEquation_eq_map_emit line 768