OAI/Computability/BinPacking/Arithmetic/GraphTallyMachine.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.BinaryEncoding.parseOption line 12
  2. def OAI.BinPackingGap.BinaryEncoding.extensionBits line 19
  3. def OAI.BinPackingGap.BinaryEncoding.parseAssignments line 22
  4. def OAI.BinPackingGap.BinaryEncoding.parseRawPacking line 24
  5. def OAI.BinPackingGap.BinaryEncoding.parseRawReductionOutput line 29
  6. def OAI.BinPackingGap.BinaryEncoding.parseExtension line 32
  7. def OAI.BinPackingGap.BinaryEncoding.decodeAssignments line 35
  8. def OAI.BinPackingGap.BinaryEncoding.decodeRawPacking line 36
  9. def OAI.BinPackingGap.BinaryEncoding.decodePackingResult line 37
  10. def OAI.BinPackingGap.BinaryEncoding.decodeRawReductionOutput line 38
  11. def OAI.BinPackingGap.BinaryEncoding.decodeExtension line 39
  12. theorem OAI.BinPackingGap.BinaryEncoding.natBits_length line 41
  13. theorem OAI.BinPackingGap.BinaryEncoding.parseNat_natBits line 44
  14. theorem OAI.BinPackingGap.BinaryEncoding.listBits_length line 48
  15. theorem OAI.BinPackingGap.BinaryEncoding.list_length_lt_bits_length line 54
  16. theorem OAI.BinPackingGap.BinaryEncoding.list_length_le_bits_length line 60
  17. theorem OAI.BinPackingGap.BinaryEncoding.pairBits_length line 64
  18. theorem OAI.BinPackingGap.BinaryEncoding.parsePair_pairBits line 68
  19. theorem OAI.BinPackingGap.BinaryEncoding.parseOption_optionBits line 77
  20. theorem OAI.BinPackingGap.BinaryEncoding.parseListAux_listBits line 83
  21. theorem OAI.BinPackingGap.BinaryEncoding.parseList_listBits line 99
  22. theorem OAI.BinPackingGap.BinaryEncoding.decode_encode line 108
  23. theorem OAI.BinPackingGap.BinaryEncoding.encode_injective line 115
  24. theorem OAI.BinPackingGap.BinaryEncoding.parseRawInstance_rawInstanceBits line 122
  25. theorem OAI.BinPackingGap.BinaryEncoding.parseAssignments_assignmentBits line 127
  26. theorem OAI.BinPackingGap.BinaryEncoding.parseRawPacking_rawPackingBits line 131
  27. theorem OAI.BinPackingGap.BinaryEncoding.parseRawReductionOutput_rawReductionOutputBits line 136
  28. theorem OAI.BinPackingGap.BinaryEncoding.parseExtension_extensionBits line 141
  29. theorem OAI.BinPackingGap.BinaryEncoding.decodeRawInstance_rawInstanceBits line 148
  30. theorem OAI.BinPackingGap.BinaryEncoding.decodeAssignments_assignmentBits line 152
  31. theorem OAI.BinPackingGap.BinaryEncoding.decodeRawPacking_rawPackingBits line 156
  32. theorem OAI.BinPackingGap.BinaryEncoding.decodePackingResult_packingResultBits line 160
  33. theorem OAI.BinPackingGap.BinaryEncoding.decodeRawReductionOutput_rawReductionOutputBits line 164
  34. theorem OAI.BinPackingGap.BinaryEncoding.decodeExtension_extensionBits line 168
  35. theorem OAI.BinPackingGap.BinaryEncoding.rawInstanceBits_injective line 175
  36. theorem OAI.BinPackingGap.BinaryEncoding.rawPackingBits_injective line 178
  37. theorem OAI.BinPackingGap.BinaryEncoding.rawInstanceBits_length line 181
  38. theorem OAI.BinPackingGap.BinaryEncoding.assignmentBits_length line 190
  39. def OAI.BinPackingGap.BinaryEncoding.ParserSound line 198
  40. theorem OAI.BinPackingGap.BinaryEncoding.parseFrame_sound line 201
  41. theorem OAI.BinPackingGap.BinaryEncoding.parseNat_sound line 230
  42. theorem OAI.BinPackingGap.BinaryEncoding.parsePair_sound line 250
  43. theorem OAI.BinPackingGap.BinaryEncoding.parseOption_sound line 270
  44. theorem OAI.BinPackingGap.BinaryEncoding.parseListAux_sound line 290
  45. theorem OAI.BinPackingGap.BinaryEncoding.parseList_sound line 322
  46. theorem OAI.BinPackingGap.BinaryEncoding.decode_sound line 327
  47. theorem OAI.BinPackingGap.BinaryEncoding.parseRawInstance_sound line 341
  48. theorem OAI.BinPackingGap.BinaryEncoding.parseAssignments_sound line 344
  49. theorem OAI.BinPackingGap.BinaryEncoding.decodeRawInstance_sound line 347
  50. theorem OAI.BinPackingGap.BinaryEncoding.decodeAssignments_sound line 351
  51. theorem OAI.BinPackingGap.BinaryEncoding.decodeExtension_sound line 355
  52. def OAI.BinPackingGap.GraphInput.endpointPairs line 373
  53. theorem OAI.BinPackingGap.GraphInput.endpointPairs_length line 376
  54. theorem OAI.BinPackingGap.GraphInput.endpointValues_injective line 380
  55. theorem OAI.BinPackingGap.GraphInput.ext_of_endpointPairs line 385
  56. structure OAI.BinPackingGap.GraphReductionInput line 400
  57. structure OAI.BinPackingGap.GraphFields line 406
  58. def OAI.BinPackingGap.GraphFields.bits line 416
  59. def OAI.BinPackingGap.GraphFields.parse line 420
  60. theorem OAI.BinPackingGap.GraphFields.parse_bits line 426
  61. def OAI.BinPackingGap.GraphFields.decode line 437
  62. theorem OAI.BinPackingGap.GraphFields.decode_bits line 439
  63. theorem OAI.BinPackingGap.GraphFields.bits_injective line 443
  64. theorem OAI.BinPackingGap.GraphFields.bits_length line 446
  65. theorem OAI.BinPackingGap.GraphFields.vertices_length_le_bits line 452
  66. theorem OAI.BinPackingGap.GraphFields.endpoints_length_le_bits line 458
  67. def OAI.BinPackingGap.GraphReductionInput.fields line 468
  68. theorem OAI.BinPackingGap.GraphReductionInput.fields_k line 471
  69. theorem OAI.BinPackingGap.GraphReductionInput.fields_vertices line 473
  70. theorem OAI.BinPackingGap.GraphReductionInput.fields_endpoints line 476
  71. theorem OAI.BinPackingGap.GraphReductionInput.fields_injective line 479
  72. def OAI.BinPackingGap.graphBits line 496
  73. theorem OAI.BinPackingGap.graphBits_eq line 498
  74. theorem OAI.BinPackingGap.parse_graphBits line 505
  75. theorem OAI.BinPackingGap.decode_graphBits line 509
  76. theorem OAI.BinPackingGap.graphBits_injective line 513
  77. theorem OAI.BinPackingGap.graph_vertexCount_le_bits line 517
  78. theorem OAI.BinPackingGap.graph_edgeCount_le_bits line 522
  79. theorem OAI.BinPackingGap.graph_k_le_bits line 527
  80. inductive OAI.BinPackingGap.GraphTallyMachine.Slot line 540
  81. instance OAI.BinPackingGap.GraphTallyMachine.(instance at line 547) line 547
  82. inductive OAI.BinPackingGap.GraphTallyMachine.Mode line 551
  83. def OAI.BinPackingGap.GraphTallyMachine.afterName line 559
  84. def OAI.BinPackingGap.GraphTallyMachine.initial line 565
  85. def OAI.BinPackingGap.GraphTallyMachine.transition line 567
  86. def OAI.BinPackingGap.GraphTallyMachine.emit line 577
  87. def OAI.BinPackingGap.GraphTallyMachine.scanOutput line 582
  88. theorem OAI.BinPackingGap.GraphTallyMachine.scanOutput_nil line 585
  89. theorem OAI.BinPackingGap.GraphTallyMachine.scanOutput_cons line 587
  90. theorem OAI.BinPackingGap.GraphTallyMachine.scanOutput_done line 591
  91. theorem OAI.BinPackingGap.GraphTallyMachine.scanOutput_frame line 597
  92. theorem OAI.BinPackingGap.GraphTallyMachine.scanOutput_natBits line 606
  93. theorem OAI.BinPackingGap.GraphTallyMachine.scanOutput_pairBits line 611
  94. theorem OAI.BinPackingGap.GraphTallyMachine.scanOutput_vertices line 616
  95. theorem OAI.BinPackingGap.GraphTallyMachine.scanOutput_endpoints line 626
  96. def OAI.BinPackingGap.GraphTallyMachine.fieldsTally line 636
  97. def OAI.BinPackingGap.GraphTallyMachine.tallyBits line 639
  98. theorem OAI.BinPackingGap.GraphTallyMachine.output_graphFields line 642
  99. def OAI.BinPackingGap.GraphTallyMachine.graphTally line 649
  100. theorem OAI.BinPackingGap.GraphTallyMachine.fieldsTally_fields line 652
  101. theorem OAI.BinPackingGap.GraphTallyMachine.output_graphBits line 657
  102. theorem OAI.BinPackingGap.GraphTallyMachine.emit_length_le line 662
  103. theorem OAI.BinPackingGap.GraphTallyMachine.scanOutput_length_le line 665
  104. theorem OAI.BinPackingGap.GraphTallyMachine.tallyBits_length_le line 675
  105. def OAI.BinPackingGap.GraphTallyMachine.reversedMachine line 680
  106. theorem OAI.BinPackingGap.GraphTallyMachine.reversedTrace line 682
  107. def OAI.BinPackingGap.GraphTallyMachine.outputsInTime_reversed line 693
  108. def OAI.BinPackingGap.GraphTallyMachine.machine line 700
  109. def OAI.BinPackingGap.GraphTallyMachine.fieldsOutputsInTime line 703
  110. def OAI.BinPackingGap.GraphTallyMachine.outputsInTime line 728
  111. def OAI.BinPackingGap.GraphTallyMachine.computableInPolyTime line 733
  112. theorem OAI.BinPackingGap.GraphTallyMachine.machine_finiteAlphabet line 750
  113. def OAI.BinPackingGap.GraphTallyMachine.tallyCopyInTime line 753