OAI/Computability/DirectedFeedback/CookLevin/NPTableau.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectedFeedback.CookLevin.Words line 12
  2. def OAI.DirectedFeedback.CookLevin.wordPush line 14
  3. def OAI.DirectedFeedback.CookLevin.wordPop line 18
  4. def OAI.DirectedFeedback.CookLevin.wordsOfLists line 20
  5. theorem OAI.DirectedFeedback.CookLevin.wordsOfLists_update line 22
  6. theorem OAI.DirectedFeedback.CookLevin.wordsOfLists_push line 31
  7. theorem OAI.DirectedFeedback.CookLevin.wordsOfLists_pop line 39
  8. structure OAI.DirectedFeedback.CookLevin.WordCfg line 47
  9. def OAI.DirectedFeedback.CookLevin.WordCfg.ofCfg line 52
  10. def OAI.DirectedFeedback.CookLevin.wordStepAux line 55
  11. theorem OAI.DirectedFeedback.CookLevin.wordStepAux_ofLists line 64
  12. def OAI.DirectedFeedback.CookLevin.radius line 78
  13. def OAI.DirectedFeedback.CookLevin.InCone line 87
  14. def OAI.DirectedFeedback.CookLevin.AgreeCone line 89
  15. theorem OAI.DirectedFeedback.CookLevin.agreeCone_mono line 93
  16. theorem OAI.DirectedFeedback.CookLevin.agreeCone_head line 102
  17. theorem OAI.DirectedFeedback.CookLevin.agreeCone_push line 106
  18. theorem OAI.DirectedFeedback.CookLevin.agreeCone_pop line 123
  19. theorem OAI.DirectedFeedback.CookLevin.wordStepAux_local line 137
  20. theorem OAI.DirectedFeedback.CookLevin.stepAux_length line 168
  21. def OAI.DirectedFeedback.CookLevin.cfgNext line 203
  22. def OAI.DirectedFeedback.CookLevin.wordNext line 208
  23. theorem OAI.DirectedFeedback.CookLevin.wordNext_ofCfg line 213
  24. def OAI.DirectedFeedback.CookLevin.programRadius line 221
  25. theorem OAI.DirectedFeedback.CookLevin.radius_le_programRadius line 225
  26. theorem OAI.DirectedFeedback.CookLevin.cfgNext_length line 228
  27. theorem OAI.DirectedFeedback.CookLevin.cfgRun_length line 239
  28. structure OAI.DirectedFeedback.CookLevin.Window line 249
  29. def OAI.DirectedFeedback.CookLevin.Window.words line 254
  30. def OAI.DirectedFeedback.CookLevin.Window.ofCfg line 257
  31. theorem OAI.DirectedFeedback.CookLevin.Window.words_ofCfg line 261
  32. def OAI.DirectedFeedback.CookLevin.Follows line 272
  33. theorem OAI.DirectedFeedback.CookLevin.window_follows line 276
  34. theorem OAI.DirectedFeedback.CookLevin.window_follows_unique line 284
  35. theorem OAI.DirectedFeedback.CookLevin.wordNext_local line 298
  36. theorem OAI.DirectedFeedback.CookLevin.trace_unique line 322
  37. theorem OAI.DirectedFeedback.CookLevin.iterate_partial_none line 347
  38. theorem OAI.DirectedFeedback.CookLevin.iterate_partial_some line 355
  39. theorem OAI.DirectedFeedback.CookLevin.cfgNext_eq_getD line 370
  40. theorem OAI.DirectedFeedback.CookLevin.output_run line 375
  41. abbrev OAI.DirectedFeedback.CookLevin.StackAtom line 397
  42. abbrev OAI.DirectedFeedback.CookLevin.Atom line 398
  43. abbrev OAI.DirectedFeedback.CookLevin.Row line 399
  44. def OAI.DirectedFeedback.CookLevin.rowWindow line 401
  45. def OAI.DirectedFeedback.CookLevin.windowRow line 406
  46. theorem OAI.DirectedFeedback.CookLevin.rowWindow_windowRow line 411
  47. structure OAI.DirectedFeedback.CookLevin.LocalData line 416
  48. def OAI.DirectedFeedback.CookLevin.LocalData.wordCfg line 421
  49. def OAI.DirectedFeedback.CookLevin.localData line 429
  50. theorem OAI.DirectedFeedback.CookLevin.localData_agree line 435
  51. theorem OAI.DirectedFeedback.CookLevin.localData_next line 449
  52. abbrev OAI.DirectedFeedback.CookLevin.StepSlot line 457
  53. abbrev OAI.DirectedFeedback.CookLevin.TracePosition line 458
  54. def OAI.DirectedFeedback.CookLevin.cellAddress line 460
  55. def OAI.DirectedFeedback.CookLevin.stepQuery line 462
  56. def OAI.DirectedFeedback.CookLevin.dataOfQueries line 469
  57. def OAI.DirectedFeedback.CookLevin.stepAccepts line 475
  58. theorem OAI.DirectedFeedback.CookLevin.dataOfQueries_eq line 483
  59. theorem OAI.DirectedFeedback.CookLevin.stepAccepts_iff line 496
  60. theorem OAI.DirectedFeedback.CookLevin.stepAccepts_all_iff line 513
  61. def OAI.DirectedFeedback.CookLevin.prefixList line 534
  62. theorem OAI.DirectedFeedback.CookLevin.prefixList_length line 540
  63. def OAI.DirectedFeedback.CookLevin.NoHoles line 550
  64. theorem OAI.DirectedFeedback.CookLevin.NoHoles.tail line 553
  65. theorem OAI.DirectedFeedback.CookLevin.NoHoles.propagate line 556
  66. theorem OAI.DirectedFeedback.CookLevin.prefixList_getElem? line 562
  67. theorem OAI.DirectedFeedback.CookLevin.prefixList_getElem?_all line 579
  68. theorem OAI.DirectedFeedback.CookLevin.list_getElem?_noHoles line 586
  69. theorem OAI.DirectedFeedback.CookLevin.reconstruct_suffix line 590
  70. def OAI.DirectedFeedback.CookLevin.InitialConditions line 618
  71. def OAI.DirectedFeedback.CookLevin.initialPredicate line 626
  72. def OAI.DirectedFeedback.CookLevin.initialQuery line 634
  73. def OAI.DirectedFeedback.CookLevin.initialAccepts line 638
  74. theorem OAI.DirectedFeedback.CookLevin.row_cell_query line 645
  75. theorem OAI.DirectedFeedback.CookLevin.initialAccepts_iff line 653
  76. theorem OAI.DirectedFeedback.CookLevin.initialAccepts_all_iff line 668
  77. theorem OAI.DirectedFeedback.CookLevin.initial_reconstruct line 695
  78. theorem OAI.DirectedFeedback.CookLevin.initial_real line 715
  79. structure OAI.DirectedFeedback.CookLevin.LocalCSP line 743
  80. def OAI.DirectedFeedback.CookLevin.LocalCSP.Satisfiable line 747
  81. structure OAI.DirectedFeedback.CookLevin.FiniteCodec line 750
  82. def OAI.DirectedFeedback.CookLevin.oneHotCodec line 756
  83. def OAI.DirectedFeedback.CookLevin.LocalCSP.booleanize line 773
  84. theorem OAI.DirectedFeedback.CookLevin.LocalCSP.booleanize_satisfiable_iff line 778
  85. def OAI.DirectedFeedback.CookLevin.LocalCSP.reindex line 789
  86. theorem OAI.DirectedFeedback.CookLevin.LocalCSP.reindex_satisfiable_iff line 794
  87. def OAI.DirectedFeedback.CookLevin.LocalCSP.pad line 807
  88. theorem OAI.DirectedFeedback.CookLevin.LocalCSP.pad_satisfiable_iff line 813
  89. abbrev OAI.DirectedFeedback.CookLevin.TableauEvent line 821
  90. abbrev OAI.DirectedFeedback.CookLevin.TableauSlot line 822
  91. def OAI.DirectedFeedback.CookLevin.tableauQuery line 824
  92. def OAI.DirectedFeedback.CookLevin.tableau line 831
  93. theorem OAI.DirectedFeedback.CookLevin.tableau_satisfiable_iff line 842
  94. theorem OAI.DirectedFeedback.CookLevin.natPoly_mono line 918
  95. def OAI.DirectedFeedback.CookLevin.NPTableau.certBound line 926
  96. def OAI.DirectedFeedback.CookLevin.NPTableau.inputBound line 927
  97. def OAI.DirectedFeedback.CookLevin.NPTableau.horizon line 928
  98. def OAI.DirectedFeedback.CookLevin.NPTableau.capacity line 929
  99. def OAI.DirectedFeedback.CookLevin.NPTableau.fixedPrefix line 932
  100. theorem OAI.DirectedFeedback.CookLevin.NPTableau.fixedPrefix_length line 935
  101. def OAI.DirectedFeedback.CookLevin.NPTableau.machine line 938
  102. def OAI.DirectedFeedback.CookLevin.NPTableau.tests line 940
  103. theorem OAI.DirectedFeedback.CookLevin.NPTableau.input_length_bound line 944
  104. theorem OAI.DirectedFeedback.CookLevin.NPTableau.run_horizon line 951
  105. theorem OAI.DirectedFeedback.CookLevin.NPTableau.tests_satisfiable_iff line 968
  106. theorem OAI.DirectedFeedback.CookLevin.NPTableau.atom_finite line 992
  107. theorem OAI.DirectedFeedback.CookLevin.NPTableau.atom_nonempty line 1002