OAI/Computability/MaxCut/Machines/CompareLoop.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

Actual finite TM2 templates for affine unary fields and finite relation bits. Commands write in forward bit order onto a stack, so their concatenated result appears reversed in the accumulator. Every unbounded operand is read from an isolated unary tape and restored by the checked preserving transducer.

  1. inductive OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.Label line 13
  2. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.Label.enumList line 18
  3. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.Label.enumList_getElem?_ctorIdx_eq line 21
  4. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.Label.enumList_nodup line 25
  5. instance OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.(instance at line 27) line 27
  6. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.statement line 34

    Source documentation

    A composable block with exactly seven internal control labels.

    def statement (labels : Label → Λ) (next : Λ) :
    Label → TM2.Stmt Alphabet Λ (State q)
  | .leftFirst => compareStatement (MachineFieldProfile.copyStatement
      (Reduction.MachineTransfer.loopAt .tail .scratch id false
        (labels .leftFirst) (some (labels .leftSecond))))
  | .leftSecond => compareStatement (MachineFieldProfile.copyStatement
      (MachineCopy.forkLoop .scratch .tail .compareLeft false
        (labels .leftSecond) (some (labels .rightFirst))))
  | .rightFirst => compareStatement (MachineFieldProfile.copyStatement
      (Reduction.MachineTransfer.loopAt .head .scratch id false
        (labels .rightFirst) (some (labels .rightSecond))))
  | .rightSecond => compareStatement (MachineFieldProfile.copyStatement
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.Label, OAI.MaxCutGames.Reduction.MachineTransfer.loopAt

  7. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.compareProgram_at_inline_CompareLoop line 53
  8. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.compareWordsInTime line 65

    Source documentation

    Compare arbitrary words while restoring every tape, including work tapes. All program hypotheses specify only the statements at the seven labels.

    def compareWordsInTime (labels : Label → Λ) (next : Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State q))
    (atLabel : ∀ label, program (labels label) = statement labels next label)
    (base : Tape → List Bool)
    (hLeft : base .compareLeft = []) (hRight : base .compareRight = [])
    (hScratch : base .scratch = [])
    (relation : GenericGraphTables.RelationTable q) (oldLoop : Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labels .leftFirst), normal relation oldLoop, base⟩
      (some ⟨some next, normal relation (decide (base .tail = base .head)), base⟩)
      (2 * ((base .tail).length + 1) + 2 * ((base .head).length + 1) +
        max (base .tail).length (base .head).length + 2) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.statement, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.RelationTable

  9. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime line 121
  10. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.encodeWord_eq_iff line 124
  11. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.compareInTime line 134

    Source documentation

    The stored flag is equality of the actual unary endpoint names.

    def compareInTime (labels : Label → Λ) (next : Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State q))
    (atLabel : ∀ label, program (labels label) = statement labels next label)
    (base : Tape → List Bool) (tailName headName : Nat)
    (hTail : base .tail = encodeWord tailName) (hHead : base .head = encodeWord headName)
    (hLeft : base .compareLeft = []) (hRight : base .compareRight = [])
    (hScratch : base .scratch = [])
    (relation : GenericGraphTables.RelationTable q) (oldLoop : Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labels .leftFirst), normal relation oldLoop, base⟩
      (some ⟨some next, normal relation (decide (tailName = headName)), base⟩)
      (comparisonTime tailName headName) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.statement, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.RelationTable, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime

  12. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime_le line 151
  13. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime_le_of_lt line 158
  14. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.compareWordsInTime_bounded line 166

    Source documentation

    A linear word-length budget, with the actual complete execution retained.

    def compareWordsInTime_bounded (labels : Label → Λ) (next : Λ)
    (program : Λ → TM2.Stmt Alphabet Λ (State q))
    (atLabel : ∀ label, program (labels label) = statement labels next label)
    (base : Tape → List Bool)
    (hLeft : base .compareLeft = []) (hRight : base .compareRight = [])
    (hScratch : base .scratch = [])
    (relation : GenericGraphTables.RelationTable q) (oldLoop : Bool)
    (N : Nat) (hTail : (base .tail).length ≤ N) (hHead : (base .head).length ≤ N) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (labels .leftFirst), normal relation oldLoop, base⟩
      (some ⟨some next, normal relation (decide (base .tail = base .head)), base⟩)
      (5 * N + 6) := by
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.statement, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.RelationTable

  15. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.rowLoop line 185
  16. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.rowState line 188
  17. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.rowLoop_eq_graph line 191
  18. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.rowContext_eq line 198
  19. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.compareRowInTime line 205
  20. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.CompareLoop.relationFromRowState line 223
  21. inductive OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Command line 252

    Source documentation

    All varying literals are finite: one Boolean or one bounded offset.

    inductive Command (h : Nat) (σ : Type) (bound : Nat)
  | literal (word : List Bool)
  | bit (value : σ → Bool)
  | bounded (value : σ → Fin bound)
  | scaled (source : Fin h) (coefficient : Nat)
  | scaledIf (source : Fin h) (coefficient : Nat) (active : σ → Bool)
  22. inductive OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Phase line 259
  23. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Alphabet line 264
  24. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.State line 265
  25. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.transition line 267
  26. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.payload line 268
  27. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.commandBits line 271
  28. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.commandSteps line 280
  29. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.commandStatement line 291

    Source documentation

    A literal Boolean is emitted by a real finite branch. A bounded offset is dispatched to a finite label, whose push chain has a fixed length.

    def commandStatement (sources : Fin h → K) (scratch output : K)
    (labels : Phase bound → Λ) (next : Λ) (command : Command h σ bound) :
    Phase bound → TM2.Stmt (Alphabet (K := K)) Λ (State σ)
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Phase, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Command, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Alphabet, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.State

  30. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.output_encodeWord_inline_Emitter line 325
  31. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.commandTrace line 341

    Source documentation

    Exact execution of one command of the supplied actual program. The only program hypotheses are equations for its concrete finite statements.

    theorem commandTrace (sources : Fin h → K) (scratch output : K)
    (sourceScratch : ∀ i, sources i ≠ scratch)
    (sourceOutput : ∀ i, sources i ≠ output) (scratchOutput : scratch ≠ output)
    (labels : Phase bound → Λ) (next : Λ) (command : Command h σ bound)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Phase, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Command, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.program, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Alphabet, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.State

  32. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Label line 418
  33. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.labelAt line 420
  34. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.commandAt line 423
  35. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.statement line 427
  36. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.program line 437
  37. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.machine line 444

    Source documentation

    Bundling makes the fixed finite tape, control-label, and register sets explicit. Neither the label type nor the state type contains a natural input.

    def machine [Fintype K] [Fintype σ] {count : Nat}
    (commands : Fin count → Command h σ bound) (sources : Fin h → K)
    (scratch output input : K) (ambient : σ) : FinTM2 where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Command

  38. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.prefixBits line 457
  39. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.prefixSteps line 463
  40. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes line 468
  41. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes_output line 471
  42. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes_other line 475
  43. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.prefixTrace line 481

    Source documentation

    Composition of the actual finite command traces, with preserved operand stacks available again at every command boundary.

    theorem prefixTrace {count : Nat} (commands : Fin count → Command h σ bound)
    (sources : Fin h → K) (scratch output : K)
    (sourceScratch : ∀ i, sources i ≠ scratch)
    (sourceOutput : ∀ i, sources i ≠ output) (scratchOutput : scratch ≠ output)
    (labels : Label count bound → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Command, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Alphabet, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.State

  44. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.planTrace line 521

    Source documentation

    The complete callable program, including its actual final jump or halt.

    theorem planTrace {count : Nat} (commands : Fin count → Command h σ bound)
    (sources : Fin h → K) (scratch output : K)
    (sourceScratch : ∀ i, sources i ≠ scratch)
    (sourceOutput : ∀ i, sources i ≠ output) (scratchOutput : scratch ≠ output)
    (labels : Label count bound → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Command, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Alphabet, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.State

  45. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.prefixSteps_le line 542
  46. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.planInTime line 562

    Source documentation

    A linear bound in the largest unary input field; plan size is fixed.

    def planInTime {count : Nat} (commands : Fin count → Command h σ bound)
    (sources : Fin h → K) (scratch output : K)
    (sourceScratch : ∀ i, sources i ≠ scratch)
    (sourceOutput : ∀ i, sources i ≠ output) (scratchOutput : scratch ≠ output)
    (labels : Label count bound → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Command, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Alphabet, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.State

  47. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.listCommands line 583
  48. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.prefixBits_listCommands line 586
  49. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.bits_listCommands line 598
  50. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands line 604
  51. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.affineValue line 608
  52. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.scaleBits_inline_Emitter line 611
  53. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands_bits line 621
  54. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands_length line 629
  55. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.bitCommands line 634

    Source documentation

    The finite relation table is encoded one actual Boolean branch at a time.

    def bitCommands (bits : List (σ → Bool)) : List (Command h σ bound) := bits.map .bit

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Command

  56. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.bitCommands_bits line 636
  57. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.affineInTime line 646

    Source documentation

    The affine template itself has an actual composable machine certificate.

    def affineInTime (terms : List (Fin h × Nat)) (offset : σ → Fin bound)
    (sources : Fin h → K) (scratch output : K)
    (sourceScratch : ∀ i, sources i ≠ scratch)
    (sourceOutput : ∀ i, sources i ≠ output) (scratchOutput : scratch ≠ output)
    (labels : Label (affineCommands terms offset).length bound → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Label, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Alphabet, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.State

  58. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Command.mapAmbient line 671

    Source documentation

    Enlarge the finite ambient registers by reading a projection of them.

    def Command.mapAmbient {τ : Type} (view : σ → τ) :
    Command h τ bound → Command h σ bound
  | .literal word => .literal word
  | .bit value => .bit (value ∘ view)
  | .bounded value => .bounded (value ∘ view)
  | .scaled source coefficient => .scaled source coefficient
  | .scaledIf source coefficient active => .scaledIf source coefficient (active ∘ view)

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.Command

  59. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.commandBits_mapAmbient line 679
  60. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Emitter.commandSteps_mapAmbient line 685
  61. abbrev OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.Terms line 707
  62. structure OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.Field line 709
  63. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.values line 713
  64. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.eval line 715
  65. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound line 719

    Source documentation

    One q-only bound covers every coefficient and every finite offset.

    def fieldBound (q : Nat) : Nat :=
…
  66. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound_pos line 722
  67. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.tapeCount_lt_bound line 726
  68. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.pairTapeCount_lt_bound line 730
  69. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.localCount_lt_bound line 734
  70. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.local_add_pair_lt_bound line 738
  71. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.twelve_local_lt_bound line 742
  72. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.zeroOffset line 746
  73. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.eventOffset line 748
  74. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryOffset line 752
  75. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.reverseOffset line 758
  76. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices line 768
  77. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts line 771
  78. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField line 774
  79. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.vertexQueryTerms line 778
  80. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.edgeQueryTerms line 781
  81. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms line 784
  82. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryField line 788
  83. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField line 791
  84. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices_eval line 795
  85. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts_eval line 801
  86. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField_eval line 806
  87. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryField_eval line 813
  88. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField_eval line 829
  89. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms line 839
  90. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_query line 843
  91. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.queryEventOffset line 851
  92. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent line 856

    Source documentation

    The sole predicate-dependent component is a bounded finite-state offset.

    def fieldForQueryEvent (q : Nat) (event : AlphabetGraph.LocalEvent (Fin q))
    (slot : Fin 6) (P : Fin q → Fin q → Bool) : Field (fieldBound q) :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.AlphabetGraph.LocalEvent, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.Field, OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound

  93. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eq_rawQueryField line 860
  94. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eval line 867
  95. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eval_verifier line 876
  96. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms line 885
  97. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.dartTailOffset line 889
  98. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldForDartTail line 893
  99. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.fieldForDartTail_eval line 897
  100. def OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.CoefficientsBounded line 909
  101. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices_coefficients line 912
  102. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts_coefficients line 919
  103. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField_coefficients line 925
  104. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_coefficients line 932
  105. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms_coefficients line 950
  106. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField_coefficients line 954
  107. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_length_le line 962
  108. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms_length_le line 968
  109. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms_coefficients line 972
  110. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms_length_le line 979
  111. theorem OAI.MaxCutGames.Foundations.PCP.AlphabetTable.Addresses.offset_lt line 986