OAI/Computability/MinUncut/Games/FinalCNFHeader.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerFrame line 12
  2. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerInputTapes line 24
  3. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes line 27
  4. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_input line 32
  5. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_archive line 35
  6. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_accumulator line 38
  7. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_rowIndex line 42
  8. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerTimePolynomial line 45
  9. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerTimePolynomial_eval line 48
  10. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerInTime line 52
  11. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.tableRowsBits line 181
  12. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.tableBits_header_rows line 184
  13. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.tableHeaderInTime line 190
  14. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headerInput_configuration line 201
  15. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.initializedTableHeaderInTime line 210
  16. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.endpointTapes line 221
  17. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.endpointsInTime line 227
  18. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.relationInTime line 252
  19. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.emitInTime line 266
  20. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.finishTapes line 283
  21. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.finishInTime line 288
  22. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow line 329
  23. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_tail line 333
  24. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_reverseIndex line 336
  25. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_relation line 339
  26. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows line 342
  27. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_get line 345
  28. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_reverseAt line 349
  29. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_acceptsAt line 356
  30. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_valid line 363
  31. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable line 371
  32. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_vertices line 377
  33. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_darts line 380
  34. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_row line 383
  35. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tail line 386
  36. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_reverseIndex line 391
  37. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_relation line 396
  38. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_words line 401
  39. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_rowList line 404
  40. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tableWords line 410
  41. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tableBits line 416
  42. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_tail line 420
  43. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_reverse line 424
  44. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_head line 429
  45. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_accepts line 435
  46. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headIndex line 440
  47. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headValue line 444
  48. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headValue_tableGraph line 450
  49. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_pattern_relation line 456
  50. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_zero line 469
  51. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_one line 470
  52. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_two line 471
  53. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_three line 472
  54. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_four line 473
  55. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_five line 474
  56. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowOperands line 476
  57. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowRelation line 480
  58. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowRest line 483
  59. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.preparedTapes line 486
  60. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_input line 492
  61. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_head line 498
  62. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_tail line 506
  63. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_reverse line 512
  64. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_frame line 519
  65. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.emittedTapes line 527
  66. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResultTapes line 533
  67. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_input line 537
  68. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_tail line 542
  69. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_head line 547
  70. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_reverse line 552
  71. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_index line 557
  72. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_accumulator line 562
  73. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_frame line 569
  74. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.guardRowInTime line 580
  75. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.guardEndInTime line 593
  76. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_operands line 604
  77. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowOperands_bounded line 633
  78. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowTime line 644
  79. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFMachine.Program.rowInTime line 647