OAI/Computability/MinUncut/Games/FinalCNFStream.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents line 10
  2. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents line 13
  3. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream line 16
  4. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream line 19
  5. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_zero line 24
  6. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_length line 28
  7. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_done line 32
  8. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_cons line 36
  9. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_zero line 43
  10. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_done line 46
  11. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_succ line 50
  12. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.processed_append_remaining line 57
  13. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_nil line 61
  14. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_cons line 63
  15. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_append line 68
  16. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_nil line 73
  17. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_cons line 76
  18. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_append line 82
  19. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_remaining_cons line 88
  20. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_remaining_cons line 95
  21. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_processed_succ line 103
  22. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_split line 112
  23. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_split line 118
  24. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.encodeWords_flatMap_rows line 124
  25. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowList_eq_finRange_map line 130
  26. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_all line 136
  27. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_remaining_zero line 148
  28. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_accumulator_succ line 152
  29. structure OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.LoopInvariant line 163
  30. structure OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.LoopRun line 174
  31. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowInvariant_succ line 186
  32. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowWords_nonempty line 206
  33. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.loopInTime line 210
  34. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.emittedBytes line 267
  35. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rawBudget line 271
  36. structure OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.RawRun line 276
  37. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.header_loopInvariant line 284
  38. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rawRun line 299
  39. inductive OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.Reference line 347
  40. structure OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.LiteralTemplate line 352
  41. abbrev OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.ClauseTemplate line 357
  42. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.queryLiteral line 359
  43. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.auxiliaryLiteral line 362
  44. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.tautologyTemplate line 365
  45. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.chainTemplates line 368
  46. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.blockTemplates line 381
  47. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.templates line 384
  48. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.literalAt line 387
  49. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.templates_length line 391
  50. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.templates_true line 394
  51. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.templates_false line 397
  52. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.literalTemplates line 400
  53. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.literalTemplates_length line 403
  54. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.literalWords line 408
  55. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.clauseWords line 411
  56. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.words line 414
  57. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.words_length line 417
  58. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.resolve line 426
  59. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.resolve_query_value line 430
  60. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.resolve_auxiliary_value line 434
  61. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.instantiateLiteral line 442
  62. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.instantiateClause line 445
  63. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.splitLong_twelve line 449
  64. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.instantiate_templates line 464
  65. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.instantiate_templates_of_acceptance line 478
  66. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.instantiateClause_words line 485
  67. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.words_eq_block line 489
  68. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTemplate.block_words_length line 497
  69. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.referenceValue line 508
  70. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.auxiliaryFlag line 512
  71. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.tailFlag line 516
  72. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headFlag line 520
  73. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.pattern_lt line 524
  74. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.referenceOffset line 528
  75. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan line 532
  76. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan_length line 541
  77. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan_bits line 544
  78. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.patternLiteral line 572
  79. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan line 577
  80. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan line 581
  81. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan_length line 584
  82. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan_length line 595
  83. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.encodeWords_flatMap line 604
  84. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan_bits line 610
  85. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.referenceValue_eq_resolve line 641
  86. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan_bits line 667