OAI/Computability/DirectedFeedback/Encoding/CompareLoop.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.Label line 12
2. instance OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.(instance at line 17) line 17
3. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.statement line 24
4. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.compareProgram_at_inline_CompareLoop line 43
5. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.compareWordsInTime line 53
6. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime line 109
7. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.encodeWord_eq_iff line 112
8. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.compareInTime line 121
9. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime_le line 138
10. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime_le_of_lt line 145
11. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.compareWordsInTime_bounded line 152
12. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.rowLoop line 171
13. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.rowState line 174
14. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.rowLoop_eq_graph line 177
15. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.rowContext_eq line 184
16. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.compareRowInTime line 191
17. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.CompareLoop.relationFromRowState line 209
18. inductive OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.Command line 230
19. inductive OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.Phase line 237
20. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.Alphabet line 242
21. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.State line 243
22. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.transition line 245
23. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.payload line 246
24. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.commandBits line 249
25. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.commandSteps line 258
26. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.commandStatement line 267
27. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.output_encodeWord_inline_Emitter line 301
28. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.commandTrace line 315
29. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.Label line 392
30. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.labelAt line 394
31. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.commandAt line 397
32. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.statement line 401
33. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.program line 411
34. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.machine line 416
35. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.prefixBits line 429
36. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.prefixSteps line 435
37. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes line 440
38. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes_output line 443
39. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes_other line 447
40. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.prefixTrace line 451
41. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.planTrace line 490
42. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.prefixSteps_le line 511
43. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.planInTime line 530
44. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.listCommands line 551
45. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.prefixBits_listCommands line 554
46. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.bits_listCommands line 566
47. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands line 572
48. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.affineValue line 576
49. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.scaleBits_inline_Emitter line 579
50. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands_bits line 589
51. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands_length line 597
52. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.bitCommands line 601
53. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.bitCommands_bits line 603
54. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.affineInTime line 612
55. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.Command.mapAmbient line 636
56. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.commandBits_mapAmbient line 644
57. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Emitter.commandSteps_mapAmbient line 650
58. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.Terms line 662
59. structure OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.Field line 664
60. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.values line 668
61. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.eval line 670
62. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound line 673
63. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound_pos line 676
64. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.tapeCount_lt_bound line 680
65. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.pairTapeCount_lt_bound line 684
66. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.localCount_lt_bound line 688
67. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.local_add_pair_lt_bound line 692
68. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.twelve_local_lt_bound line 696
69. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.zeroOffset line 700
70. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.eventOffset line 702
71. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryOffset line 706
72. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.reverseOffset line 712
73. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices line 722
74. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts line 725
75. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField line 728
76. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.vertexQueryTerms line 732
77. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.edgeQueryTerms line 735
78. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms line 738
79. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryField line 742
80. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField line 745
81. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices_eval line 749
82. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts_eval line 755
83. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField_eval line 760
84. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryField_eval line 767
85. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField_eval line 783
86. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms line 793
87. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_query line 797
88. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.queryEventOffset line 805
89. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent line 809
90. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eq_rawQueryField line 813
91. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eval line 820
92. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eval_verifier line 829
93. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms line 838
94. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.dartTailOffset line 842
95. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.fieldForDartTail line 846
96. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.fieldForDartTail_eval line 850
97. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.CoefficientsBounded line 862
98. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices_coefficients line 865
99. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts_coefficients line 872
100. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField_coefficients line 878
101. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_coefficients line 885
102. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms_coefficients line 903
103. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField_coefficients line 907
104. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_length_le line 915
105. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms_length_le line 921
106. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms_coefficients line 925
107. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms_length_le line 932
108. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Addresses.offset_lt line 939