OAI/Computability/PerfectCompleteness/Machines/FiniteBlockMachineLemmas.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.FiniteBlockMachine.encode line 24
  2. theorem OAI.PerfectCompleteness.FiniteBlockMachine.encode_injective line 27
  3. def OAI.PerfectCompleteness.FiniteBlockMachine.decode line 33
  4. theorem OAI.PerfectCompleteness.FiniteBlockMachine.decode_encode line 36
  5. def OAI.PerfectCompleteness.FiniteBlockMachine.word line 42
  6. theorem OAI.PerfectCompleteness.FiniteBlockMachine.word_length line 44
  7. def OAI.PerfectCompleteness.FiniteBlockMachine.transform line 47
  8. theorem OAI.PerfectCompleteness.FiniteBlockMachine.transform_encode line 51
  9. def OAI.PerfectCompleteness.FiniteBlockMachine.statement line 56
  10. theorem OAI.PerfectCompleteness.FiniteBlockMachine.statement_trace line 61
  11. theorem OAI.PerfectCompleteness.FiniteBlockMachine.statement_pushBound line 74
  12. def OAI.PerfectCompleteness.FiniteBlockMachine.machine line 80
  13. theorem OAI.PerfectCompleteness.FiniteBlockMachine.machine_step line 84
  14. def OAI.PerfectCompleteness.FiniteBlockMachine.computation line 110
  15. theorem OAI.PerfectCompleteness.FiniteBlockMachine.machine_pushBound line 127
  16. theorem OAI.PerfectCompleteness.FiniteBlockMachine.machine_workAlphabet_finite line 132
  17. abbrev OAI.PerfectCompleteness.FiniteReadMachine.State line 154
  18. theorem OAI.PerfectCompleteness.FiniteReadMachine.state_finite line 156
  19. def OAI.PerfectCompleteness.FiniteReadMachine.saveFinish line 159
  20. theorem OAI.PerfectCompleteness.FiniteReadMachine.saveFinish_pushBound line 165
  21. theorem OAI.PerfectCompleteness.FiniteReadMachine.stepAux_saveFinish line 170
  22. def OAI.PerfectCompleteness.FiniteReadMachine.statement line 182
  23. theorem OAI.PerfectCompleteness.FiniteReadMachine.statement_trace line 187
  24. theorem OAI.PerfectCompleteness.FiniteReadMachine.statement_pushBound line 201
  25. theorem OAI.PerfectCompleteness.FiniteReadMachine.step line 206
  26. def OAI.PerfectCompleteness.FiniteReadMachine.inTime line 221
  27. abbrev OAI.PerfectCompleteness.FiniteWordMachine.State line 251
  28. def OAI.PerfectCompleteness.FiniteWordMachine.keys line 253
  29. theorem OAI.PerfectCompleteness.FiniteWordMachine.keys_complete line 255
  30. def OAI.PerfectCompleteness.FiniteWordMachine.literalTable line 258
  31. def OAI.PerfectCompleteness.FiniteWordMachine.cleanFinish line 262
  32. theorem OAI.PerfectCompleteness.FiniteWordMachine.cleanFinish_pushBound line 266
  33. theorem OAI.PerfectCompleteness.FiniteWordMachine.stepAux_cleanFinish line 270
  34. def OAI.PerfectCompleteness.FiniteWordMachine.statement line 279
  35. theorem OAI.PerfectCompleteness.FiniteWordMachine.statement_trace line 286
  36. theorem OAI.PerfectCompleteness.FiniteWordMachine.statement_pushBound line 307
  37. def OAI.PerfectCompleteness.FiniteWordMachine.machine line 318
  38. theorem OAI.PerfectCompleteness.FiniteWordMachine.machine_step line 329
  39. def OAI.PerfectCompleteness.FiniteWordMachine.computation line 352
  40. theorem OAI.PerfectCompleteness.FiniteWordMachine.machine_pushBound line 369
  41. theorem OAI.PerfectCompleteness.FiniteWordMachine.machine_workAlphabet_finite line 375
  42. def OAI.PerfectCompleteness.KeyMetadataEncoding.bitWord line 391
  43. theorem OAI.PerfectCompleteness.KeyMetadataEncoding.bitWord_eq_iff line 393
  44. theorem OAI.PerfectCompleteness.KeyMetadataEncoding.bitWord_le line 396
  45. def OAI.PerfectCompleteness.KeyMetadataEncoding.entryID line 399
  46. def OAI.PerfectCompleteness.KeyMetadataEncoding.entryWords line 404
  47. theorem OAI.PerfectCompleteness.KeyMetadataEncoding.entryWords_length line 411
  48. theorem OAI.PerfectCompleteness.KeyMetadataEncoding.entryWords_injective line 416
  49. def OAI.PerfectCompleteness.KeyMetadataEncoding.metadataWords line 424
  50. theorem OAI.PerfectCompleteness.KeyMetadataEncoding.metadataWords_nil line 427
  51. theorem OAI.PerfectCompleteness.KeyMetadataEncoding.metadataWords_cons line 429
  52. theorem OAI.PerfectCompleteness.KeyMetadataEncoding.metadataWords_length line 433
  53. theorem OAI.PerfectCompleteness.KeyMetadataEncoding.metadataWords_injective line 442
  54. theorem OAI.PerfectCompleteness.KeyMetadataEncoding.entryWords_le line 468
  55. theorem OAI.PerfectCompleteness.KeyMetadataEncoding.metadataWords_le line 493
  56. def OAI.PerfectCompleteness.CanonicalKeyEncoding.reducedValueEquiv line 511
  57. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.reducedValue_card line 528
  58. abbrev OAI.PerfectCompleteness.CanonicalKeyEncoding.Assignment line 532
  59. def OAI.PerfectCompleteness.CanonicalKeyEncoding.partitionWidth line 534
  60. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.partitionWidth_eq line 536
  61. def OAI.PerfectCompleteness.CanonicalKeyEncoding.partEnum line 540
  62. def OAI.PerfectCompleteness.CanonicalKeyEncoding.partitionMask line 543
  63. def OAI.PerfectCompleteness.CanonicalKeyEncoding.partitionOfMask line 547
  64. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.partitionOfMask_partitionMask line 550
  65. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.partitionMask_injective line 556
  66. def OAI.PerfectCompleteness.CanonicalKeyEncoding.boolWord line 561
  67. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.boolWord_injective line 563
  68. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.boolWord_le_one line 567
  69. def OAI.PerfectCompleteness.CanonicalKeyEncoding.partitionWords line 570
  70. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.partitionWords_length line 573
  71. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.partitionWords_injective line 576
  72. def OAI.PerfectCompleteness.CanonicalKeyEncoding.sideWord line 584
  73. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.sideWord_injective line 588
  74. def OAI.PerfectCompleteness.CanonicalKeyEncoding.words line 592
  75. def OAI.PerfectCompleteness.CanonicalKeyEncoding.bits line 596
  76. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.words_length line 598
  77. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.bits_length_le line 604
  78. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.words_injective line 621
  79. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.bits_injective line 637
  80. def OAI.PerfectCompleteness.CanonicalKeyEncoding.sameEncoding line 641
  81. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.sameEncoding_eq_true_iff line 643
  82. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.bits_eq_iff line 648
  83. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.key_retained_length_le line 651
  84. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.key_bits_length_le line 660
  85. theorem OAI.PerfectCompleteness.CanonicalKeyEncoding.bits_projection line 673