OAI/Computability/BinPacking/PCP/Lookup.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.Alphabet line 13
  2. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.State line 14
  3. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.relationEquiv line 16
  4. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.relationFintype line 22
  5. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.stateFintype line 25
  6. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlot line 30
  7. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readSlot line 40
  8. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlots line 50
  9. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.indexedWords line 56
  10. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots line 59
  11. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_preserves_correct line 65
  12. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_mem line 77
  13. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_finRange line 90
  14. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.indexedWords_finRange line 97
  15. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readSlots line 109
  16. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.readRelation line 125
  17. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readRelation line 130
  18. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readRelation_fromTapes line 141
  19. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlots_pushBound line 155
  20. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.readRelation_pushBound line 165
  21. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.parser line 171
  22. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.parser_pushBound line 176
  23. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.parserStep line 181
  24. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.parserTrace line 195
  25. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.ReadRelation.parserInTime line 207
  26. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.Alphabet line 232
  27. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.skipBits line 234
  28. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.stepAux_skipBits line 245
  29. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.stepAux_skipBits_fromTapes line 262
  30. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.skipBits_pushBound line 276
  31. inductive OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.Label line 284
  32. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.Label.enumList line 288
  33. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.Label.enumList_getElem?_ctorIdx_eq line 291
  34. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.Label.enumList_nodup line 295
  35. instance OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.(instance at line 297) line 297
  36. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.statement line 301
  37. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.program line 310
  38. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.rowBits line 314
  39. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.rowBits_eq line 316
  40. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits line 321
  41. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits_nil line 324
  42. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits_cons line 326
  43. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.skipCost line 330
  44. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.prefixCost line 333
  45. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.lookupCost line 336
  46. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.skipRowTrace line 348
  47. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.skipRowTrace_fromTapes line 377
  48. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.selectTrace line 391
  49. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.lookupTailTrace line 409
  50. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.lookupCost_le line 477
  51. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.lookupTailInTime line 496
  52. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.tableTailTrace line 519
  53. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.fullTableTailTrace line 551
  54. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.lookup_frame line 591
  55. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.tableTailCost line 597
  56. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.tableTailCost_le line 601
  57. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.headIndex line 624
  58. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.headValue line 627
  59. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.headValue_eq_semantics line 630
  60. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.HeadTapes line 633
  61. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes line 635
  62. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.headLookupCost line 644
  63. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.headLookupCost_le line 648
  64. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.headTimePolynomial line 657
  65. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.headLookupInTime line 660
  66. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes_head line 752
  67. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes_frame line 757
  68. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes line 763
  69. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_source line 768
  70. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_tail line 774
  71. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_reverse line 780
  72. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_frame line 786
  73. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost line 792
  74. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost_le line 795
  75. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost_table_le line 802
  76. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.readRowInTime line 811
  77. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Lookup.machine line 895