OAI/Computability/DirectedFeedback/Machines/FinalCNFHeader.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerFrame line 56
  2. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerInputTapes line 68
  3. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes line 71
  4. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_input line 76
  5. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_archive line 79
  6. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_accumulator line 82
  7. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_rowIndex line 86
  8. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerTimePolynomial line 89
  9. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerTimePolynomial_eval line 92
  10. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerInTime line 96
  11. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.tableRowsBits line 225
  12. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.tableBits_header_rows line 228
  13. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.tableHeaderInTime line 234
  14. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headerInput_configuration line 245
  15. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.initializedTableHeaderInTime line 254
  16. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.endpointTapes line 273
  17. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.endpointsInTime line 279
  18. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.relationInTime line 304
  19. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.emitInTime line 318
  20. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.finishTapes line 335
  21. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.finishInTime line 340
  22. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow line 384
  23. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_tail line 388
  24. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_reverseIndex line 391
  25. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_relation line 394
  26. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows line 397
  27. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_get line 400
  28. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_reverseAt line 404
  29. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_acceptsAt line 411
  30. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_valid line 418
  31. def OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable line 426
  32. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_vertices line 432
  33. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_darts line 435
  34. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_row line 438
  35. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tail line 441
  36. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_reverseIndex line 446
  37. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_relation line 451
  38. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_words line 456
  39. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_rowList line 459
  40. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tableWords line 465
  41. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tableBits line 471
  42. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_tail line 475
  43. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_reverse line 479
  44. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_head line 484
  45. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_accepts line 490
  46. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headIndex line 495
  47. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headValue line 499
  48. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headValue_tableGraph line 505
  49. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_pattern_relation line 511
  50. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_zero line 527
  51. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_one line 528
  52. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_two line 529
  53. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_three line 530
  54. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_four line 531
  55. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_five line 532
  56. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowOperands line 534
  57. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowRelation line 538
  58. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowRest line 541
  59. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.preparedTapes line 544
  60. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_input line 550
  61. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_head line 556
  62. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_tail line 564
  63. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_reverse line 570
  64. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_frame line 577
  65. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.emittedTapes line 585
  66. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowResultTapes line 591
  67. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_input line 595
  68. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_tail line 600
  69. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_head line 605
  70. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_reverse line 610
  71. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_index line 615
  72. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_accumulator line 620
  73. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_frame line 627
  74. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.guardRowInTime line 638
  75. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.guardEndInTime line 651
  76. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_operands line 662
  77. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowOperands_bounded line 691
  78. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowTime line 702
  79. def OAI.DFVSGames.Foundations.Complexity.FinalCNFMachine.Program.rowInTime line 705