OAI/Computability/DirectedFeedback/Encoding/Body.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.bodyTime line 15
  2. structure OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.RowStepResult line 18
  3. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.guardTapes line 28
  4. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.parsedTapes line 32
  5. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.workingTapes line 37
  6. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.emittedTapes line 41
  7. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.clearFieldsTapes line 46
  8. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.resultTapes line 49
  9. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.workingTapes_other_inline_Body line 54
  10. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.workingTapes_counter_inline_Body line 64
  11. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.workingTapes_cursor_inline_Body line 70
  12. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.workingTapes_tail_inline_Body line 76
  13. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.workingTapes_reverse_inline_Body line 82
  14. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.workingTapes_head_inline_Body line 88
  15. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.clearFieldsInTime line 95
  16. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.incrementInTime line 117
  17. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.emitterView_at_inline_Body line 132
  18. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.context_rowState_inline_Body line 142
  19. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.emitInTime line 151
  20. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.result_ready_inline_Body line 189
  21. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.workingOperands_inline_Body line 200
  22. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Body.rowStep line 210
  23. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.inputTapes line 335
  24. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.rowsBits line 339
  25. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.headerBits line 342
  26. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.setupTapes line 346
  27. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.loopTapes line 354
  28. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.loopStart line 363
  29. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.setupResult_eq line 367
  30. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.headerResult_eq line 373
  31. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.machineInitial_eq line 378
  32. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.setupInTime line 388
  33. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.headerView_at_inline_Initialization line 407
  34. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.headerInTime line 417
  35. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.time line 455
  36. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.time_eq line 457
  37. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Initialization.initializeInTime line 461
  38. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.LoopInitialization.initialization_ready line 480
  39. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Loop.zeroGuardInTime line 515
  40. structure OAI.DFVSGames.Foundations.PCP.AlphabetTable.Loop.LoopResult line 529
  41. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Loop.runRemaining line 541
  42. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Loop.prefixTime line 573
  43. structure OAI.DFVSGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult line 576
  44. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Loop.runPrefix line 586
  45. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult.reversed line 609
  46. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult.output line 613
  47. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.afterReversal line 626
  48. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_output line 629
  49. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_reversed line 633
  50. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.finishBudget line 637
  51. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.reverseInTime line 640
  52. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.cleared_eq_haltList line 655
  53. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.cleanupInTime line 662
  54. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.finishInTime line 678
  55. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_selected_length_le line 699
  56. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.stackLength_after_prefix line 706
  57. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.finishBudget_le_of_prefix line 718
  58. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.completedPolynomial line 740
  59. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.finishAfterPrefix line 745
  60. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Finish.finishAfterPolynomialPrefix line 761
  61. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Runtime.prefixPolynomial line 784
  62. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Runtime.prefixPolynomial_eval line 790
  63. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Runtime.time line 797
  64. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Runtime.tableOutputsInTime line 800
  65. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Runtime.tablePolynomialTime line 816