OAI/Computability/DirectedFeedback/Encoding/NameCompaction.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.PCP.NameCompaction.clauseNames line 11
2. def OAI.DFVSGames.Foundations.PCP.NameCompaction.sourceNames line 14
3. def OAI.DFVSGames.Foundations.PCP.NameCompaction.activeNames line 17
4. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.literal_mem_active line 20
5. def OAI.DFVSGames.Foundations.PCP.NameCompaction.compactIndex line 29
6. def OAI.DFVSGames.Foundations.PCP.NameCompaction.decodeName line 33
7. def OAI.DFVSGames.Foundations.PCP.NameCompaction.compactLiteral line 36
8. def OAI.DFVSGames.Foundations.PCP.NameCompaction.compactClause line 40
9. def OAI.DFVSGames.Foundations.PCP.NameCompaction.compactClauses line 46
10. def OAI.DFVSGames.Foundations.PCP.NameCompaction.compact line 49
11. def OAI.DFVSGames.Foundations.PCP.NameCompaction.restrictAssignment line 53
12. def OAI.DFVSGames.Foundations.PCP.NameCompaction.extendAssignment line 56
13. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.decode_compactIndex line 60
14. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.eval_compact_restrict line 64
15. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.eval_compact_extend line 70
16. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.map_attach_val line 80
17. def OAI.DFVSGames.Foundations.PCP.NameCompaction.evaluationList line 84
18. def OAI.DFVSGames.Foundations.PCP.NameCompaction.satisfiedCount line 87
19. def OAI.DFVSGames.Foundations.PCP.NameCompaction.failedCount line 90
20. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.evaluationList_restrict line 93
21. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.evaluationList_extend line 99
22. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.satisfiedCount_restrict line 110
23. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.failedCount_restrict line 114
24. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.satisfiedCount_extend line 118
25. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.failedCount_extend line 122
26. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.clauseNames_flat_length line 126
27. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.compact_clause_count line 135
28. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.length_eraseDups_le line 139
29. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.compact_active_bound line 153
30. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.compact_completeness line 158
31. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.compact_reflects line 167
32. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.compact_satisfiable_iff line 178
33. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.compact_preserves_gap line 182
34. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.compact_encoding_bound line 189
35. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.failureCount_evaluations line 207
36. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.evaluations_allIndices line 217
37. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.verifier_failureCount line 225
38. theorem OAI.DFVSGames.Foundations.PCP.NameCompaction.compact_verifier_soundness line 230
39. def OAI.DFVSGames.BinaryFormula.sourceNames line 251
40. def OAI.DFVSGames.BinaryFormula.activeNames line 254
41. theorem OAI.DFVSGames.BinaryFormula.literal_mem_active line 257
42. def OAI.DFVSGames.BinaryFormula.compactIndex line 265
43. def OAI.DFVSGames.BinaryFormula.decodeName line 269
44. def OAI.DFVSGames.BinaryFormula.compactLiteral line 272
45. def OAI.DFVSGames.BinaryFormula.compactClause line 276
46. def OAI.DFVSGames.BinaryFormula.compactClauses line 282
47. def OAI.DFVSGames.BinaryFormula.dense line 285
48. def OAI.DFVSGames.BinaryFormula.restrictAssignment line 289
49. def OAI.DFVSGames.BinaryFormula.extendAssignment line 292
50. theorem OAI.DFVSGames.BinaryFormula.decode_compactIndex line 296
51. theorem OAI.DFVSGames.BinaryFormula.compactIndex_injective line 300
52. theorem OAI.DFVSGames.BinaryFormula.compactLiteral_positive line 306
53. theorem OAI.DFVSGames.BinaryFormula.eval_compact_restrict line 309
54. theorem OAI.DFVSGames.BinaryFormula.eval_compact_extend line 315
55. def OAI.DFVSGames.BinaryFormula.evaluationList line 324
56. theorem OAI.DFVSGames.BinaryFormula.evaluationList_restrict line 327
57. theorem OAI.DFVSGames.BinaryFormula.evaluationList_extend line 335
58. def OAI.DFVSGames.BinaryFormula.failedCount line 349
59. theorem OAI.DFVSGames.BinaryFormula.failedCount_restrict line 352
60. theorem OAI.DFVSGames.BinaryFormula.failedCount_extend line 356
61. theorem OAI.DFVSGames.BinaryFormula.clauseNames_flat_length line 360
62. theorem OAI.DFVSGames.BinaryFormula.dense_clause_count line 369
63. theorem OAI.DFVSGames.BinaryFormula.dense_variable_bound line 373
64. theorem OAI.DFVSGames.BinaryFormula.dense_completeness line 378
65. theorem OAI.DFVSGames.BinaryFormula.dense_reflects line 387
66. theorem OAI.DFVSGames.BinaryFormula.dense_satisfiable_iff line 397
67. theorem OAI.DFVSGames.BinaryFormula.dense_preserves_gap line 401
68. theorem OAI.DFVSGames.BinaryFormula.dense_encoding_bound line 408
69. theorem OAI.DFVSGames.BinaryEncoding.dense_encoding_bound line 432
70. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCompare.Alphabet line 452
71. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCompare.State line 453
72. def OAI.DFVSGames.Foundations.Complexity.MachineCompare.exitAt line 455
73. def OAI.DFVSGames.Foundations.Complexity.MachineCompare.finish line 460
74. def OAI.DFVSGames.Foundations.Complexity.MachineCompare.loop line 463
75. def OAI.DFVSGames.Foundations.Complexity.MachineCompare.mismatch line 473
76. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.mismatch_nil_nil line 476
77. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.mismatch_nil_cons line 479
78. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.mismatch_cons_nil line 482
79. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.mismatch_true line 485
80. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.mismatch_cons line 488
81. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.stepAux_exitAt line 493
82. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.stepAux_finish line 498
83. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.update_left_inline_MachineCompare line 504
84. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.update_right_inline_MachineCompare line 517
85. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.step_empty line 523
86. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.step_nil_cons line 540
87. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.step_cons_nil line 555
88. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.step_cons_cons line 570
89. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.trace_left_empty_inline_MachineCompare line 587
90. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.compareTrace_flag line 612
91. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.compareTrace line 647
92. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.compareTrace_fromTapes line 662
93. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.drained_other line 675
94. def OAI.DFVSGames.Foundations.Complexity.MachineCompare.compareInTime line 679
95. theorem OAI.DFVSGames.Foundations.Complexity.MachineCompare.compareInTime_steps line 694