OAI/Computability/BinPacking/Search/ExtensionValidationMachine.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.ExtensionValidationMachine.validRows line 9
  2. theorem OAI.BinPackingGap.ExtensionValidationMachine.validRows_eq line 16
  3. inductive OAI.BinPackingGap.ExtensionValidationMachine.ScanCall line 29
  4. abbrev OAI.BinPackingGap.ExtensionValidationMachine.ScanCall.enumList line 33
  5. theorem OAI.BinPackingGap.ExtensionValidationMachine.ScanCall.enumList_getElem?_ctorIdx_eq line 35
  6. theorem OAI.BinPackingGap.ExtensionValidationMachine.ScanCall.enumList_nodup line 39
  7. instance OAI.BinPackingGap.ExtensionValidationMachine.(instance at line 41) line 41
  8. abbrev OAI.BinPackingGap.ExtensionValidationMachine.ScanPhase line 45
  9. inductive OAI.BinPackingGap.ExtensionValidationMachine.OrderCall line 47
  10. abbrev OAI.BinPackingGap.ExtensionValidationMachine.OrderCall.enumList line 51
  11. theorem OAI.BinPackingGap.ExtensionValidationMachine.OrderCall.enumList_getElem?_ctorIdx_eq line 53
  12. theorem OAI.BinPackingGap.ExtensionValidationMachine.OrderCall.enumList_nodup line 57
  13. instance OAI.BinPackingGap.ExtensionValidationMachine.(instance at line 59) line 59
  14. inductive OAI.BinPackingGap.ExtensionValidationMachine.Control line 63
  15. abbrev OAI.BinPackingGap.ExtensionValidationMachine.Control.enumList line 68
  16. theorem OAI.BinPackingGap.ExtensionValidationMachine.Control.enumList_getElem?_ctorIdx_eq line 71
  17. theorem OAI.BinPackingGap.ExtensionValidationMachine.Control.enumList_nodup line 75
  18. instance OAI.BinPackingGap.ExtensionValidationMachine.(instance at line 77) line 77
  19. inductive OAI.BinPackingGap.ExtensionValidationMachine.Label line 81
  20. abbrev OAI.BinPackingGap.ExtensionValidationMachine.Tape line 87
  21. abbrev OAI.BinPackingGap.ExtensionValidationMachine.Alphabet line 88
  22. abbrev OAI.BinPackingGap.ExtensionValidationMachine.State line 89
  23. def OAI.BinPackingGap.ExtensionValidationMachine.clean line 91
  24. def OAI.BinPackingGap.ExtensionValidationMachine.scanSource line 93
  25. def OAI.BinPackingGap.ExtensionValidationMachine.scanOutput line 98
  26. def OAI.BinPackingGap.ExtensionValidationMachine.scanTape line 104
  27. def OAI.BinPackingGap.ExtensionValidationMachine.scanPorts line 109
  28. theorem OAI.BinPackingGap.ExtensionValidationMachine.scanPorts_apply line 115
  29. def OAI.BinPackingGap.ExtensionValidationMachine.orderTape line 120
  30. def OAI.BinPackingGap.ExtensionValidationMachine.orderPorts line 127
  31. def OAI.BinPackingGap.ExtensionValidationMachine.scanSuccess line 132
  32. def OAI.BinPackingGap.ExtensionValidationMachine.orderExit line 138
  33. def OAI.BinPackingGap.ExtensionValidationMachine.jump line 144
  34. def OAI.BinPackingGap.ExtensionValidationMachine.controlInstruction line 147
  35. def OAI.BinPackingGap.ExtensionValidationMachine.program line 176
  36. abbrev OAI.BinPackingGap.ExtensionValidationMachine.machine line 183
  37. def OAI.BinPackingGap.ExtensionValidationMachine.cfg line 194
  38. def OAI.BinPackingGap.ExtensionValidationMachine.work line 197
  39. def OAI.BinPackingGap.ExtensionValidationMachine.ready line 207
  40. theorem OAI.BinPackingGap.ExtensionValidationMachine.update_items line 211
  41. theorem OAI.BinPackingGap.ExtensionValidationMachine.update_assignments line 215
  42. theorem OAI.BinPackingGap.ExtensionValidationMachine.update_numerator line 219
  43. theorem OAI.BinPackingGap.ExtensionValidationMachine.update_denominator line 223
  44. theorem OAI.BinPackingGap.ExtensionValidationMachine.update_assigned line 227
  45. def OAI.BinPackingGap.ExtensionValidationMachine.oneStep line 231
  46. def OAI.BinPackingGap.ExtensionValidationMachine.join line 240
  47. def OAI.BinPackingGap.ExtensionValidationMachine.enlarge line 248
  48. def OAI.BinPackingGap.ExtensionValidationMachine.scanInTime line 255
  49. def OAI.BinPackingGap.ExtensionValidationMachine.orderInTime line 267
  50. theorem OAI.BinPackingGap.ExtensionValidationMachine.markerStep line 279
  51. theorem OAI.BinPackingGap.ExtensionValidationMachine.boundEndStep line 290
  52. theorem OAI.BinPackingGap.ExtensionValidationMachine.positiveStep line 301
  53. theorem OAI.BinPackingGap.ExtensionValidationMachine.endStep line 311
  54. def OAI.BinPackingGap.ExtensionValidationMachine.clearInTime line 319
  55. def OAI.BinPackingGap.ExtensionValidationMachine.numeratorInTime line 338
  56. def OAI.BinPackingGap.ExtensionValidationMachine.denominatorInTime line 350
  57. def OAI.BinPackingGap.ExtensionValidationMachine.assignedInTime line 362
  58. theorem OAI.BinPackingGap.ExtensionValidationMachine.fractionExit line 374
  59. theorem OAI.BinPackingGap.ExtensionValidationMachine.boundExit line 380
  60. theorem OAI.BinPackingGap.ExtensionValidationMachine.bits_eq_nil_iff line 386
  61. def OAI.BinPackingGap.ExtensionValidationMachine.rowBudget line 395
  62. def OAI.BinPackingGap.ExtensionValidationMachine.loopTime line 398
  63. structure OAI.BinPackingGap.ExtensionValidationMachine.LoopRun line 402
  64. def OAI.BinPackingGap.ExtensionValidationMachine.rowsInTime line 413
  65. theorem OAI.BinPackingGap.ExtensionValidationMachine.base_budget line 525
  66. theorem OAI.BinPackingGap.ExtensionValidationMachine.row_budget line 533
  67. theorem OAI.BinPackingGap.ExtensionValidationMachine.loopTime_le line 537
  68. def OAI.BinPackingGap.ExtensionValidationMachine.inputTapes line 563
  69. def OAI.BinPackingGap.ExtensionValidationMachine.initializeInTime line 567
  70. def OAI.BinPackingGap.ExtensionValidationMachine.inputLength line 587
  71. def OAI.BinPackingGap.ExtensionValidationMachine.validationTime line 591
  72. theorem OAI.BinPackingGap.ExtensionValidationMachine.total_budget line 593
  73. theorem OAI.BinPackingGap.ExtensionValidationMachine.totalTime_le line 610
  74. theorem OAI.BinPackingGap.ExtensionValidationMachine.flagStep line 620
  75. structure OAI.BinPackingGap.ExtensionValidationMachine.ValidationRun line 633
  76. def OAI.BinPackingGap.ExtensionValidationMachine.validationInTime line 643
  77. theorem OAI.BinPackingGap.ExtensionValidationMachine.machine_finiteAlphabet line 657