OAI/Computability/DirectedFeedback/Machines/FinalCNFStream.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents line 55
  2. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents line 58
  3. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream line 61
  4. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream line 64
  5. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_zero line 69
  6. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_length line 73
  7. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_done line 77
  8. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_cons line 81
  9. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_zero line 88
  10. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_done line 91
  11. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_succ line 95
  12. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.processed_append_remaining line 102
  13. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_nil line 106
  14. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_cons line 108
  15. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_append line 113
  16. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_nil line 118
  17. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_cons line 121
  18. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_append line 127
  19. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_remaining_cons line 133
  20. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_remaining_cons line 140
  21. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_processed_succ line 148
  22. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_split line 157
  23. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_split line 163
  24. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.encodeWords_flatMap_rows_inline_FinalCNFStream line 169
  25. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowList_eq_finRange_map line 175
  26. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_all line 181
  27. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_remaining_zero line 191
  28. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_accumulator_succ line 195
  29. structure OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.LoopInvariant line 214
  30. structure OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.LoopRun line 225
  31. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowInvariant_succ line 237
  32. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowWords_nonempty line 257
  33. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.loopInTime line 261
  34. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.emittedBytes line 325
  35. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rawBudget line 329
  36. structure OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.RawRun line 334
  37. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.header_loopInvariant line 342
  38. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rawRun line 357
  39. inductive OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.Reference line 409
  40. structure OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.LiteralTemplate line 414
  41. abbrev OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.ClauseTemplate line 419
  42. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.queryLiteral line 421
  43. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.auxiliaryLiteral line 424
  44. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.tautologyTemplate line 427
  45. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.chainTemplates line 430
  46. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.blockTemplates line 443
  47. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.templates line 446
  48. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.literalAt line 449
  49. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.templates_length line 453
  50. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.templates_true line 456
  51. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.templates_false line 459
  52. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.literalTemplates line 462
  53. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.literalTemplates_length line 465
  54. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.literalWords line 470
  55. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.clauseWords line 473
  56. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.words line 476
  57. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.words_length line 479
  58. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.resolve line 488
  59. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.resolve_query_value line 492
  60. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.resolve_auxiliary_value line 496
  61. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.instantiateLiteral line 504
  62. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.instantiateClause line 507
  63. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.splitLong_twelve line 511
  64. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.instantiate_templates line 526
  65. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.instantiate_templates_of_acceptance line 540
  66. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.instantiateClause_words line 547
  67. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.words_eq_block line 551
  68. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTemplate.block_words_length line 559
  69. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.referenceValue line 574
  70. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.auxiliaryFlag line 578
  71. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.tailFlag line 582
  72. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headFlag line 586
  73. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.pattern_lt line 590
  74. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.referenceOffset line 594
  75. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan line 598
  76. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan_length line 607
  77. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan_bits line 610
  78. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.patternLiteral line 638
  79. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan line 643
  80. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan line 647
  81. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan_length line 650
  82. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan_length line 661
  83. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.encodeWords_flatMap line 668
  84. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan_bits line 674
  85. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.referenceValue_eq_resolve line 705
  86. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan_bits line 731
  87. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader line 760
  88. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader_eq line 763
  89. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_eq_formulaHeader line 769
  90. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_eq_clauseBits line 775
  91. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.header_append_outputStream line 794
  92. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.emitted_output_eq line 800
  93. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.reversed_accumulator_output line 809
  94. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.accumulator_length_bound line 814