OAI/Computability/BinPacking/Reductions/BinaryRenameWords.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingCompleteness.BinaryNameSearch.Token line 13
  2. def OAI.BinPackingCompleteness.BinaryNameSearch.tokenBits line 15
  3. def OAI.BinPackingCompleteness.BinaryNameSearch.stream line 18
  4. def OAI.BinPackingCompleteness.BinaryNameSearch.payloads line 22
  5. def OAI.BinPackingCompleteness.BinaryNameSearch.afterMatch line 24
  6. def OAI.BinPackingCompleteness.BinaryNameSearch.steps line 28
  7. def OAI.BinPackingCompleteness.BinaryNameSearch.payloadSize line 34
  8. theorem OAI.BinPackingCompleteness.BinaryNameSearch.stream_nil line 36
  9. theorem OAI.BinPackingCompleteness.BinaryNameSearch.stream_cons line 38
  10. theorem OAI.BinPackingCompleteness.BinaryNameSearch.payloads_nil line 41
  11. theorem OAI.BinPackingCompleteness.BinaryNameSearch.payloads_cons line 43
  12. theorem OAI.BinPackingCompleteness.BinaryNameSearch.payloadSize_nil line 46
  13. theorem OAI.BinPackingCompleteness.BinaryNameSearch.payloadSize_cons line 48
  14. theorem OAI.BinPackingCompleteness.BinaryNameSearch.stream_length line 51
  15. theorem OAI.BinPackingCompleteness.BinaryNameSearch.steps_le line 60
  16. theorem OAI.BinPackingCompleteness.BinaryNameSearch.steps_le_stream line 69
  17. abbrev OAI.BinPackingCompleteness.BinaryNameSearch.Alphabet line 79
  18. abbrev OAI.BinPackingCompleteness.BinaryNameSearch.State line 80
  19. abbrev OAI.BinPackingCompleteness.BinaryNameSearch.clean line 82
  20. inductive OAI.BinPackingCompleteness.BinaryNameSearch.Label line 84
  21. def OAI.BinPackingCompleteness.BinaryNameSearch.compareTapes line 90
  22. theorem OAI.BinPackingCompleteness.BinaryNameSearch.compareTapes_injective line 93
  23. def OAI.BinPackingCompleteness.BinaryNameSearch.exitAt line 100
  24. def OAI.BinPackingCompleteness.BinaryNameSearch.finish line 105
  25. def OAI.BinPackingCompleteness.BinaryNameSearch.instruction line 108
  26. theorem OAI.BinPackingCompleteness.BinaryNameSearch.stepAux_finish line 119
  27. theorem OAI.BinPackingCompleteness.BinaryNameSearch.update_source line 123
  28. theorem OAI.BinPackingCompleteness.BinaryNameSearch.update_counter line 134
  29. theorem OAI.BinPackingCompleteness.BinaryNameSearch.joinTrace line 140
  30. theorem OAI.BinPackingCompleteness.BinaryNameSearch.signStep line 153
  31. theorem OAI.BinPackingCompleteness.BinaryNameSearch.emptyStep line 164
  32. theorem OAI.BinPackingCompleteness.BinaryNameSearch.incrementStep line 174
  33. theorem OAI.BinPackingCompleteness.BinaryNameSearch.tokenTrace line 190
  34. theorem OAI.BinPackingCompleteness.BinaryNameSearch.searchTrace line 236
  35. def OAI.BinPackingCompleteness.BinaryNameSearch.searchInTime line 287
  36. def OAI.BinPackingCompleteness.BinaryNameSearch.machine line 308
  37. theorem OAI.BinPackingCompleteness.BinaryNameSearch.machine_finiteAlphabet line 321
  38. def OAI.BinPackingCompleteness.BinaryRenameWords.clauseLiterals line 331
  39. def OAI.BinPackingCompleteness.BinaryRenameWords.literals line 333
  40. def OAI.BinPackingCompleteness.BinaryRenameWords.token line 335
  41. def OAI.BinPackingCompleteness.BinaryRenameWords.tokens line 338
  42. theorem OAI.BinPackingCompleteness.BinaryRenameWords.literals_nil line 341
  43. theorem OAI.BinPackingCompleteness.BinaryRenameWords.literals_cons line 343
  44. theorem OAI.BinPackingCompleteness.BinaryRenameWords.literals_length line 346
  45. theorem OAI.BinPackingCompleteness.BinaryRenameWords.tokens_length line 352
  46. theorem OAI.BinPackingCompleteness.BinaryRenameWords.literals_names line 355
  47. theorem OAI.BinPackingCompleteness.BinaryRenameWords.tokens_payloads line 360
  48. theorem OAI.BinPackingCompleteness.BinaryRenameWords.token_bits line 365
  49. theorem OAI.BinPackingCompleteness.BinaryRenameWords.tokens_stream line 370
  50. theorem OAI.BinPackingCompleteness.BinaryRenameWords.tokens_canonical line 381
  51. theorem OAI.BinPackingCompleteness.BinaryRenameWords.payload_index line 387
  52. theorem OAI.BinPackingCompleteness.BinaryRenameWords.token_payload_mem line 392
  53. theorem OAI.BinPackingCompleteness.BinaryRenameWords.payloadSize_tokens line 399
  54. def OAI.BinPackingCompleteness.BinaryRenameWords.outputLiteral line 412
  55. def OAI.BinPackingCompleteness.BinaryRenameWords.body line 416
  56. theorem OAI.BinPackingCompleteness.BinaryRenameWords.encoded_clause line 419
  57. theorem OAI.BinPackingCompleteness.BinaryRenameWords.encodeWords_flatMap line 427
  58. theorem OAI.BinPackingCompleteness.BinaryRenameWords.encoded_body line 434
  59. theorem OAI.BinPackingCompleteness.BinaryRenameWords.encoded_renamed line 447