OAI/Computability/MaxCut/Estimates/Basic.lean

GitHub source file

151 declarations, 0 contain sorry, 0 declared as axioms

Actual regular-table construction

The header subroutine reads the two original graph headers, computes the padding total by the actual prefix machine, performs unary addition and constant multiplication, and appends both resulting header fields. The outer vertex routines are assembled from actual metadata and row programs.

  1. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Extra line 22
  2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Extra.enumList line 26
  3. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Extra.enumList_getElem?_ctorIdx_eq line 29
  4. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Extra.enumList_nodup line 33
  5. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 35) line 35
  6. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Tape line 39
  7. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Alphabet line 40
  8. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.State line 41
  9. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.tableTape line 43
  10. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.nTape line 44
  11. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.queryTape line 45
  12. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.fuelTape line 46
  13. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.sumTape line 47
  14. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.mTape line 48
  15. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.indexTape line 49
  16. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.workTape line 50
  17. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.scratchTape line 51
  18. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.verticesTape line 52
  19. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.dartsTape line 53
  20. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.emitTape line 54
  21. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.outputTape line 55
  22. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.memory line 57
  23. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame line 69
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame_table line 72
  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame_n line 74
  26. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame_query line 76
  27. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame_fuel line 78
  28. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame_sum line 80
  29. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame_m line 82
  30. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame_index line 84
  31. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame_work line 86
  32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame_scratch line 88
  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame_vertices line 90
  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame_darts line 92
  35. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame_emit line 94
  36. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame_output line 96
  37. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_table line 99
  38. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_n line 112
  39. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_query line 125
  40. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_fuel line 138
  41. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_sum line 151
  42. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_m line 164
  43. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_index line 177
  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_work line 190
  45. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_scratch line 203
  46. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_vertices line 216
  47. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_darts line 229
  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_emit line 242
  49. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_output line 255
  50. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Field line 268
  51. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Field.enumList line 272
  52. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Field.enumList_getElem?_ctorIdx_eq line 274
  53. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Field.enumList_nodup line 278
  54. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 280) line 280
  55. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase line 284
  56. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase.enumList line 288
  57. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase.enumList_getElem?_ctorIdx_eq line 290
  58. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase.enumList_nodup line 294
  59. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 296) line 296
  60. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Label line 300
  61. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.fieldTape line 310
  62. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.fieldExit line 314
  63. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.lookupSlots line 318
  64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.lookupSlots_injective line 321
  65. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.copySource line 326
  66. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.copyDestination line 331
  67. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.copyExit line 335
  68. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.prefixView line 340
  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.prefixView_left line 344
  70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.prefixView_right line 346
  71. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.prefixTapes line 350
  72. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.program line 361
  73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.appendTrace_inline_MachineRegularTable line 391
  74. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.paddingTotal line 395
  75. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.vertexTotal line 398
  76. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.dartTotal line 401
  77. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.vertexTotal_eq line 403
  78. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.initStep line 408
  79. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.seedMStep line 417
  80. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.clearIndexStep line 426
  81. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.readTime line 435
  82. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.readTrace line 440

    Source documentation

    Both original header numbers are produced by physical preserving lookups.

    theorem readTrace (q : Nat) (t : GraphTables.Table) (output : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program q)))^[readTime t]
      (some ⟨some .init, ((ambient, false), register),
        frame (GraphTables.tableBits t) [] [] [] [] [] [] [] [] [] [] [] output⟩) =
      some ⟨some (.prefix .init), ((ambient, false), none),
        frame (GraphTables.tableBits t) (encodeWord t.vertices) [] [] []
          (encodeWord t.darts) [] [] [] [] [] [] output⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.readTime, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  83. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.prefixTrace line 489

    Source documentation

    The original vertex count is the physical bound supplied to the checked padding-prefix machine. Its complement tapes preserve the original dart count.

    theorem prefixTrace (q : Nat) (t : GraphTables.Table) (output : List Bool)
    (ambient : σ) (register : Option Bool) :
    (advance (TM2.step (program q)))^[MachineCloudPrefix.totalTime t t.vertices []]
      (some ⟨some (.prefix .init), ((ambient, false), register),
        frame (GraphTables.tableBits t) (encodeWord t.vertices) [] [] []
          (encodeWord t.darts) [] [] [] [] [] [] output⟩) =
      some ⟨some (.copyFirst .count), ((ambient, false), none),
        frame (GraphTables.tableBits t) (encodeWord t.vertices) (encodeWord t.vertices)
          (encodeWord 0) (encodeWord (paddingTotal t)) (encodeWord t.darts)
          [] [] [] [] [] [] output⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.program, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPrefix.totalTime, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.paddingTotal

  84. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.computeTime line 509
  85. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.computeTrace line 512
  86. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.headerBits line 550
  87. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.headerBits_eq line 553
  88. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.headerBits_length line 557
  89. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.cleanupZerosStep line 563
  90. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.emitTime line 572
  91. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.emitTrace line 576
  92. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.totalTime line 639
  93. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.trace line 642
  94. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.arithmeticPolynomial line 655
  95. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.timePolynomial line 662
  96. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.totalTime_le line 665
  97. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.inTime line 708

    Source documentation

    A genuine finite-machine execution with a cubic input-length budget.

    def inTime (q : Nat) (t : GraphTables.Table) (output : List Bool)
    (ambient : σ) (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (program q))
      ⟨some .init, ((ambient, false), register),
        frame (GraphTables.tableBits t) [] [] [] [] [] [] [] [] [] [] [] output⟩
      (some ⟨none, ((ambient, false), none),
        frame (GraphTables.tableBits t) (encodeWord t.vertices) [] [] [] (encodeWord t.darts)
          [] [] [] (encodeWord (vertexTotal t)) (encodeWord (dartTotal q t)) []
          (output ++ headerBits q t)⟩)
      ((timePolynomial q).eval ((GraphTables.tableBits t).length + output.length)) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.frame, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.vertexTotal, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.dartTotal, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.headerBits, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.timePolynomial

  98. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Fuel.guard line 730

    Source documentation

    The outer loop consumes one real unary fuel bit. The zero delimiter is consumed on exit; its temporary finite register is reset on both branches.

    def guard (fuel : K) (body : Λ) (exit : Option Λ) :
    TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool) :=
…
  99. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Fuel.guard_succ line 738
  100. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Fuel.guard_zero line 745
  101. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Fuel.increment line 753

    Source documentation

    Unary successor needs one physical push and no unbounded register.

    def increment (counter : K) (next : Λ) : TM2.Stmt (fun _ : K => Bool) Λ σ :=
…
  102. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Fuel.increment_step line 756
  103. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.Body line 766
  104. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.Tape line 767
  105. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.Alphabet line 768
  106. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.State line 769
  107. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.Data line 770
  108. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.BaseTable line 771
  109. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.sumDecidableEq_inline_MachineRegularTable line 773
  110. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.tapeDecidableEq line 784
  111. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.tapeBEq line 799
  112. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.tapeLawfulBEq line 802
  113. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.tapeFintype line 806
  114. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.coreTape line 814
  115. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldFuel line 815
  116. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerFuel line 816
  117. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.dummyFuel line 817
  118. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.scratch line 818
  119. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerTape line 820
  120. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerView line 826
  121. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerView_left line 837
  122. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerView_right line 846
  123. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.bodyView line 865
  124. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.bodyView_left line 869
  125. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.bodyView_right line 870
  126. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerTape line 876
  127. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerView line 880
  128. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerView_left line 888
  129. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.ownerView_right line 894
  130. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerStates line 903
  131. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.readyState line 911
  132. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase line 913
  133. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase.enumList line 916
  134. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase.enumList_getElem?_ctorIdx_eq line 918
  135. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase.enumList_nodup line 922
  136. instance OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.(instance at line 924) line 924
  137. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.copySource line 928
  138. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.copyTarget line 931
  139. inductive OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.Label line 935
  140. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.copyExit line 950
  141. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.clearTape line 954
  142. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.clearEntry line 958
  143. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.program line 963

    Source documentation

    All graph-dependent loop counts remain on tapes. The code contains only the fixed expander base and the finite subprogram labels.

    def program (H : BaseTable) : Label → TM2.Stmt Alphabet Label State
  | .header l => Lift.statement headerTape Label.header (some .oldSeed) headerStates
      (Header.program PreprocessingRegularTables.internalDegree l)
  | .oldSeed => .push (coreTape 1) (fun _ => false) (.goto fun _ => Label.copyFirst CopyPhase.old)
  | .copyFirst phase => Reduction.MachineTransfer.loopAt (copySource phase) scratch id false
      (.copyFirst phase) (some (.copySecond phase))
  | .copySecond phase => MachineCopy.forkLoop scratch (copySource phase) (copyTarget phase) false
      (.copySecond phase) (some (copyExit phase))
  | .oldGuard => Fuel.guard oldFuel (Label.oldBody MachineRegularOriginalBody.entry) (some Label.ownerSeed)
  | .oldBody l => Lift.statement Sum.inl Label.oldBody (some .oldIncrement) (Equiv.refl _)
      (MachineRegularOriginalBody.program H l)
  | .oldIncrement => Fuel.increment (coreTape 1) Label.oldGuard
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.BaseTable, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.Label, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.State, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Lift.statement, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerTape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerStates, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.coreTape, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.copySource, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.scratch, OAI.MaxCutGames.Foundations.Complexity.MachineCopy.forkLoop, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.copyTarget, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.copyExit, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Fuel.guard, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.oldFuel, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.entry, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.program, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Fuel.increment

  144. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.machine line 983
  145. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.frame line 996

    Source documentation

    These are mathematical descriptions of the physical stacks at loop boundaries. They are never loaded into the machine's finite control.

    def frame (data : Data) (header : Header.Tape → List Bool) (counters : Fin 4 → List Bool) :
    Tape → List Bool
  | .inl k => MachineRegularOriginalBody.frame data k
  | .inr (.inl k) => header k
  | .inr (.inr i) => counters i

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.Data, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Header.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.Tape, OAI.MaxCutGames.Foundations.Complexity.MachineRegularOriginalBody.frame

  146. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.cfg line 1002
  147. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.frame_core line 1007
  148. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.bodyPlacement line 1011
  149. def OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerAux line 1020
  150. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerAux_empty line 1026
  151. theorem OAI.MaxCutGames.Foundations.Complexity.MachineRegularTable.Top.headerPlacement line 1030