OAI/Computability/BinPacking/Reductions/BinaryNameCompare.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingCompleteness.BinaryNameMachine.frame line 13
  2. def OAI.BinPackingCompleteness.BinaryNameMachine.finalDigit line 17
  3. def OAI.BinPackingCompleteness.BinaryNameMachine.canonical line 21
  4. structure OAI.BinPackingCompleteness.BinaryNameMachine.Result line 23
  5. def OAI.BinPackingCompleteness.BinaryNameMachine.scanSpec line 29
  6. def OAI.BinPackingCompleteness.BinaryNameMachine.steps line 35
  7. theorem OAI.BinPackingCompleteness.BinaryNameMachine.steps_le line 39
  8. theorem OAI.BinPackingCompleteness.BinaryNameMachine.frame_length line 48
  9. theorem OAI.BinPackingCompleteness.BinaryNameMachine.scanSpec_frame line 54
  10. theorem OAI.BinPackingCompleteness.BinaryNameMachine.steps_frame line 63
  11. abbrev OAI.BinPackingCompleteness.BinaryNameMachine.Alphabet line 73
  12. abbrev OAI.BinPackingCompleteness.BinaryNameMachine.State line 74
  13. def OAI.BinPackingCompleteness.BinaryNameMachine.clean line 76
  14. def OAI.BinPackingCompleteness.BinaryNameMachine.exitAt line 78
  15. def OAI.BinPackingCompleteness.BinaryNameMachine.finish line 83
  16. def OAI.BinPackingCompleteness.BinaryNameMachine.scan line 86
  17. theorem OAI.BinPackingCompleteness.BinaryNameMachine.stepAux_finish line 101
  18. theorem OAI.BinPackingCompleteness.BinaryNameMachine.update_source line 106
  19. theorem OAI.BinPackingCompleteness.BinaryNameMachine.update_destination line 117
  20. theorem OAI.BinPackingCompleteness.BinaryNameMachine.step_empty line 131
  21. theorem OAI.BinPackingCompleteness.BinaryNameMachine.step_end line 139
  22. theorem OAI.BinPackingCompleteness.BinaryNameMachine.step_truncated line 150
  23. theorem OAI.BinPackingCompleteness.BinaryNameMachine.step_digit line 158
  24. theorem OAI.BinPackingCompleteness.BinaryNameMachine.scanTrace line 168
  25. def OAI.BinPackingCompleteness.BinaryNameMachine.scanInTime line 202
  26. theorem OAI.BinPackingCompleteness.BinaryNameMachine.framedTrace line 214
  27. def OAI.BinPackingCompleteness.BinaryNameMachine.machine line 227
  28. theorem OAI.BinPackingCompleteness.BinaryNameMachine.machine_finiteAlphabet line 238
  29. def OAI.BinPackingCompleteness.BinaryNameMachine.machineInTime line 242
  30. abbrev OAI.BinPackingCompleteness.BinaryNameCompare.Alphabet line 262
  31. abbrev OAI.BinPackingCompleteness.BinaryNameCompare.State line 263
  32. def OAI.BinPackingCompleteness.BinaryNameCompare.clean line 265
  33. def OAI.BinPackingCompleteness.BinaryNameCompare.scanStateEquiv line 267
  34. def OAI.BinPackingCompleteness.BinaryNameCompare.compareStateEquiv line 273
  35. inductive OAI.BinPackingCompleteness.BinaryNameCompare.Label line 279
  36. abbrev OAI.BinPackingCompleteness.BinaryNameCompare.Label.enumList line 283
  37. theorem OAI.BinPackingCompleteness.BinaryNameCompare.Label.enumList_getElem?_ctorIdx_eq line 285
  38. theorem OAI.BinPackingCompleteness.BinaryNameCompare.Label.enumList_nodup line 289
  39. instance OAI.BinPackingCompleteness.BinaryNameCompare.(instance at line 291) line 291
  40. def OAI.BinPackingCompleteness.BinaryNameCompare.instruction line 295
  41. def OAI.BinPackingCompleteness.BinaryNameCompare.steps line 308
  42. theorem OAI.BinPackingCompleteness.BinaryNameCompare.steps_le line 311
  43. theorem OAI.BinPackingCompleteness.BinaryNameCompare.joinTrace line 316
  44. theorem OAI.BinPackingCompleteness.BinaryNameCompare.compareTrace line 320
  45. def OAI.BinPackingCompleteness.BinaryNameCompare.compareInTime line 424
  46. def OAI.BinPackingCompleteness.BinaryNameCompare.machine line 446
  47. theorem OAI.BinPackingCompleteness.BinaryNameCompare.machine_finiteAlphabet line 459