OAI/Computability/BinPacking/Computation/TableIterationFiniteAlphabet.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_zero line 15
  2. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_one line 16
  3. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_two line 17
  4. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_three line 18
  5. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_four line 19
  6. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_five line 20
  7. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowOperands line 22
  8. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowRelation line 26
  9. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowRest line 29
  10. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.preparedTapes line 32
  11. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_input line 38
  12. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_head line 44
  13. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_tail line 52
  14. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_reverse line 58
  15. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_frame line 65
  16. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.emittedTapes line 73
  17. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowResultTapes line 79
  18. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_input line 83
  19. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_tail line 88
  20. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_head line 93
  21. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_reverse line 98
  22. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_index line 103
  23. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_accumulator line 108
  24. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_frame line 115
  25. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.guardRowInTime line 126
  26. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.guardEndInTime line 139
  27. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_operands line 150
  28. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowOperands_bounded line 179
  29. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowTime line 190
  30. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowInTime line 193
  31. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents line 283
  32. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents line 286
  33. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream line 289
  34. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream line 292
  35. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_zero line 297
  36. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_length line 301
  37. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_done line 305
  38. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_cons line 309
  39. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_zero line 316
  40. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_done line 319
  41. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_succ line 323
  42. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.processed_append_remaining line 330
  43. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_nil line 334
  44. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_cons line 336
  45. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_append line 341
  46. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_nil line 346
  47. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_cons line 349
  48. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_append line 355
  49. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_remaining_cons line 361
  50. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_remaining_cons line 368
  51. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_processed_succ line 376
  52. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_split line 385
  53. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_split line 391
  54. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.encodeWords_flatMap_rows line 397
  55. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowList_eq_finRange_map line 403
  56. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_all line 409
  57. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_remaining_zero line 418
  58. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_accumulator_succ line 422
  59. structure OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.LoopInvariant line 437
  60. structure OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.LoopRun line 448
  61. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowInvariant_succ line 460
  62. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowWords_nonempty line 480
  63. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.loopInTime line 484
  64. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.emittedBytes line 545
  65. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rawBudget line 549
  66. structure OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.RawRun line 554
  67. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.header_loopInvariant line 562
  68. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rawRun line 577
  69. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader line 625
  70. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader_eq line 628
  71. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_eq_formulaHeader line 634
  72. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_eq_clauseBits line 640
  73. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.header_append_outputStream line 659
  74. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.emitted_output_eq line 665
  75. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.reversed_accumulator_output line 674
  76. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.accumulator_length_bound line 679
  77. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowTimePolynomial line 691
  78. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowTimePolynomial_eval line 695
  79. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowTime_expanded line 700
  80. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial line 704
  81. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial_eval line 709
  82. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial_eval_expanded line 716
  83. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTime_le line 722
  84. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.table_phaseTime_le line 730
  85. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial line 738
  86. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial_eval line 742
  87. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.finalTime_le line 748
  88. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.emittedBytes_eq_formulaBits line 760
  89. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rawBudget_le_phaseTime line 764
  90. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.computableInPolyTime line 770
  91. def OAI.BinPackingGames.Foundations.Complexity.MachineTableIteration.finalTable line 806
  92. def OAI.BinPackingGames.Foundations.Complexity.MachineTableIteration.counterCertificate line 809
  93. def OAI.BinPackingGames.Foundations.Complexity.MachineTableIteration.countedCertificate line 817
  94. def OAI.BinPackingGames.Foundations.Complexity.MachineTableIteration.computableInPolyTime line 854
  95. def OAI.BinPackingGames.Foundations.Complexity.MachineTableIteration.initialCertificate line 858
  96. def OAI.BinPackingGames.Foundations.Complexity.MachineTableIteration.tableCertificate line 864
  97. def OAI.BinPackingGames.Foundations.Complexity.MachineTableIteration.gapMapCertificate line 871
  98. theorem OAI.BinPackingGames.Foundations.Complexity.TableIterationFiniteAlphabet.initial line 883
  99. theorem OAI.BinPackingGames.Foundations.Complexity.TableIterationFiniteAlphabet.finalCNF line 888
  100. theorem OAI.BinPackingGames.Foundations.Complexity.TableIterationFiniteAlphabet.counter line 893
  101. theorem OAI.BinPackingGames.Foundations.Complexity.TableIterationFiniteAlphabet.counted line 905
  102. theorem OAI.BinPackingGames.Foundations.Complexity.TableIterationFiniteAlphabet.iteration line 908
  103. theorem OAI.BinPackingGames.Foundations.Complexity.TableIterationFiniteAlphabet.table line 912
  104. theorem OAI.BinPackingGames.Foundations.Complexity.TableIterationFiniteAlphabet.gapMap line 916