OAI/Computability/BinPacking/Search/ExtensionAgreementMachine.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.ExtensionAgreementMachine.Label line 10
  2. abbrev OAI.BinPackingGap.ExtensionAgreementMachine.Label.enumList line 15
  3. theorem OAI.BinPackingGap.ExtensionAgreementMachine.Label.enumList_getElem?_ctorIdx_eq line 18
  4. theorem OAI.BinPackingGap.ExtensionAgreementMachine.Label.enumList_nodup line 22
  5. instance OAI.BinPackingGap.ExtensionAgreementMachine.(instance at line 24) line 24
  6. abbrev OAI.BinPackingGap.ExtensionAgreementMachine.Alphabet line 28
  7. abbrev OAI.BinPackingGap.ExtensionAgreementMachine.State line 29
  8. def OAI.BinPackingGap.ExtensionAgreementMachine.jump line 31
  9. def OAI.BinPackingGap.ExtensionAgreementMachine.readBoth line 34
  10. def OAI.BinPackingGap.ExtensionAgreementMachine.program line 43
  11. abbrev OAI.BinPackingGap.ExtensionAgreementMachine.machine line 72
  12. def OAI.BinPackingGap.ExtensionAgreementMachine.tapes line 83
  13. def OAI.BinPackingGap.ExtensionAgreementMachine.cfg line 86
  14. theorem OAI.BinPackingGap.ExtensionAgreementMachine.update_fixed line 89
  15. theorem OAI.BinPackingGap.ExtensionAgreementMachine.update_assignments line 93
  16. structure OAI.BinPackingGap.ExtensionAgreementMachine.View line 97
  17. def OAI.BinPackingGap.ExtensionAgreementMachine.View.cfg line 102
  18. def OAI.BinPackingGap.ExtensionAgreementMachine.bothView line 105
  19. def OAI.BinPackingGap.ExtensionAgreementMachine.next line 112
  20. def OAI.BinPackingGap.ExtensionAgreementMachine.Terminal line 141
  21. instance OAI.BinPackingGap.ExtensionAgreementMachine.(instance at line 143) line 143
  22. def OAI.BinPackingGap.ExtensionAgreementMachine.rank line 146
  23. def OAI.BinPackingGap.ExtensionAgreementMachine.potential line 152
  24. theorem OAI.BinPackingGap.ExtensionAgreementMachine.next_decreases line 155
  25. theorem OAI.BinPackingGap.ExtensionAgreementMachine.step_view line 162
  26. def OAI.BinPackingGap.ExtensionAgreementMachine.run line 176
  27. theorem OAI.BinPackingGap.ExtensionAgreementMachine.run_step line 181
  28. theorem OAI.BinPackingGap.ExtensionAgreementMachine.run_terminal line 185
  29. theorem OAI.BinPackingGap.ExtensionAgreementMachine.runTrace line 188
  30. theorem OAI.BinPackingGap.ExtensionAgreementMachine.run_isTerminal line 203
  31. def OAI.BinPackingGap.ExtensionAgreementMachine.resultView line 212
  32. theorem OAI.BinPackingGap.ExtensionAgreementMachine.run_drainAssignments line 215
  33. theorem OAI.BinPackingGap.ExtensionAgreementMachine.run_drainFixed line 225
  34. theorem OAI.BinPackingGap.ExtensionAgreementMachine.run_checkEnd_empty line 235
  35. theorem OAI.BinPackingGap.ExtensionAgreementMachine.run_skipFrame line 239
  36. theorem OAI.BinPackingGap.ExtensionAgreementMachine.run_compareFrame line 253
  37. abbrev OAI.BinPackingGap.ExtensionAgreementMachine.fixedBits line 284
  38. theorem OAI.BinPackingGap.ExtensionAgreementMachine.run_encoded line 287
  39. def OAI.BinPackingGap.ExtensionAgreementMachine.agreementTime line 341
  40. structure OAI.BinPackingGap.ExtensionAgreementMachine.RawRun line 343
  41. def OAI.BinPackingGap.ExtensionAgreementMachine.rawInTime line 349
  42. def OAI.BinPackingGap.ExtensionAgreementMachine.agreementInTime line 364
  43. theorem OAI.BinPackingGap.ExtensionAgreementMachine.flagStep line 377
  44. def OAI.BinPackingGap.ExtensionAgreementMachine.agreementFlagInTime line 383
  45. theorem OAI.BinPackingGap.ExtensionAgreementMachine.machine_finiteAlphabet line 405