OAI/Computability/BinPacking/Search/SearchFixedReplaceMachine.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.SearchFixedReplaceMachine.Slot line 11
  2. abbrev OAI.BinPackingGap.SearchFixedReplaceMachine.Slot.enumList line 15
  3. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.Slot.enumList_getElem?_ctorIdx_eq line 17
  4. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.Slot.enumList_nodup line 21
  5. instance OAI.BinPackingGap.SearchFixedReplaceMachine.(instance at line 23) line 23
  6. inductive OAI.BinPackingGap.SearchFixedReplaceMachine.Action line 27
  7. abbrev OAI.BinPackingGap.SearchFixedReplaceMachine.Action.enumList line 31
  8. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.Action.enumList_getElem?_ctorIdx_eq line 33
  9. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.Action.enumList_nodup line 37
  10. instance OAI.BinPackingGap.SearchFixedReplaceMachine.(instance at line 39) line 39
  11. inductive OAI.BinPackingGap.SearchFixedReplaceMachine.Label line 43
  12. def OAI.BinPackingGap.SearchFixedReplaceMachine.Action.writes line 53
  13. def OAI.BinPackingGap.SearchFixedReplaceMachine.Action.next line 57
  14. abbrev OAI.BinPackingGap.SearchFixedReplaceMachine.Words line 61
  15. abbrev OAI.BinPackingGap.SearchFixedReplaceMachine.Register line 62
  16. def OAI.BinPackingGap.SearchFixedReplaceMachine.put line 64
  17. def OAI.BinPackingGap.SearchFixedReplaceMachine.consume line 67
  18. def OAI.BinPackingGap.SearchFixedReplaceMachine.emit line 69
  19. def OAI.BinPackingGap.SearchFixedReplaceMachine.saved line 72
  20. def OAI.BinPackingGap.SearchFixedReplaceMachine.finish line 79
  21. def OAI.BinPackingGap.SearchFixedReplaceMachine.copyIf line 83
  22. def OAI.BinPackingGap.SearchFixedReplaceMachine.instruction line 88
  23. def OAI.BinPackingGap.SearchFixedReplaceMachine.tapes line 126
  24. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.tapes_at line 135
  25. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.tapes_other line 139
  26. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.update_tapes line 144
  27. def OAI.BinPackingGap.SearchFixedReplaceMachine.configuration line 159
  28. def OAI.BinPackingGap.SearchFixedReplaceMachine.next line 167
  29. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.step_eq line 209
  30. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.oneStepTrace line 257
  31. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.frame_cons_clock line 261
  32. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.joinTrace line 267
  33. def OAI.BinPackingGap.SearchFixedReplaceMachine.words line 271
  34. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.put_words line 277
  35. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.one line 288
  36. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.nameTrace line 293
  37. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.optionTrace line 325
  38. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.copyTrace line 359
  39. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.payloadTrace line 381
  40. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.drainPayloadTrace line 406
  41. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.drainIndexTrace line 427
  42. theorem OAI.BinPackingGap.SearchFixedReplaceMachine.replaceTrace line 444
  43. def OAI.BinPackingGap.SearchFixedReplaceMachine.replaceInTime line 512