OAI/Computability/BinPacking/Search/ExtensionVerifierMachine.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Block line 13
  2. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Block.enumList line 17
  3. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Block.enumList_getElem?_ctorIdx_eq line 19
  4. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Block.enumList_nodup line 23
  5. instance OAI.BinPackingGap.ExtensionVerifierMachine.Fields.(instance at line 25) line 25
  6. inductive OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Field line 29
  7. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Field.enumList line 33
  8. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Field.enumList_getElem?_ctorIdx_eq line 35
  9. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Field.enumList_nodup line 39
  10. instance OAI.BinPackingGap.ExtensionVerifierMachine.Fields.(instance at line 41) line 41
  11. inductive OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Mode line 45
  12. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Field.block line 52
  13. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.afterField line 56
  14. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Mode.block line 61
  15. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.nextMode line 66
  16. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Words line 74
  17. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.prepend line 76
  18. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.prepend_nil line 79
  19. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.prepend_prepend line 83
  20. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.run line 91
  21. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.run_frame line 96
  22. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.run_nat line 110
  23. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.run_items line 116
  24. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.run_fixed line 141
  25. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.encodedWords line 149
  26. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.empty line 154
  27. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.reversed line 156
  28. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.reversed_reversed line 158
  29. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.wordLength line 162
  30. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.wordLength_empty line 165
  31. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.wordLength_reversed line 167
  32. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.wordLength_prepend line 170
  33. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.run_wordLength line 174
  34. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.run_extension line 183
  35. inductive OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Label line 194
  36. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Label.enumList line 198
  37. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Label.enumList_getElem?_ctorIdx_eq line 201
  38. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Label.enumList_nodup line 205
  39. instance OAI.BinPackingGap.ExtensionVerifierMachine.Fields.(instance at line 207) line 207
  40. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.Fields.Alphabet line 211
  41. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.Fields.State line 212
  42. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.scanFinish line 214
  43. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.instruction line 218
  44. abbrev OAI.BinPackingGap.ExtensionVerifierMachine.Fields.machine line 232
  45. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.tapes line 243
  46. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.cfg line 252
  47. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.update_input line 256
  48. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.savedTape line 261
  49. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.outputTape line 266
  50. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.update_saved line 271
  51. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.update_output line 277
  52. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.step_scan_empty line 283
  53. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.step_scan_cons line 290
  54. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.scanTrace line 312
  55. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.initList_eq line 328
  56. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.scan_extension line 335
  57. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.restoreLabel line 343
  58. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.nextRestore line 348
  59. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.restoreTrace line 353
  60. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.appendTrace line 377
  61. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.restoreAllTrace line 381
  62. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.extensionTrace line 423
  63. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.extensionInTime line 443
  64. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.extracted line 452
  65. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.totalTrace line 455
  66. def OAI.BinPackingGap.ExtensionVerifierMachine.Fields.extractionInTime line 475
  67. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.extracted_extension line 482
  68. theorem OAI.BinPackingGap.ExtensionVerifierMachine.Fields.machine_finiteAlphabet line 488