OAI/Computability/MaxCut/Games/FinalCNFHeader.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

The concrete final-CNF machine's entry phase. It archives its complete input, reads the two unary size fields, emits the exact formula header, and reaches the row guard. The transition witness is assembled from actual program calls.

  1. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerFrame line 20

    Source documentation

    Explicit tape frame used during the header phase; all unlisted work tapes are empty. The archive is separate from the unread input.

    def headerFrame (input archive vertices darts rowIndex tail head accumulator : List Bool) :
    Tape → List Bool
  | .input => input
  | .archive => archive
  | .vertices => vertices
  | .darts => darts
  | .rowIndex => rowIndex
  | .tail => tail
  | .head => head
  | .accumulator => accumulator
  | _ => []

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape

  2. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerInputTapes line 32
  3. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes line 37

    Source documentation

    Exact row-guard handoff: the original table is protected in archive, the output header is accumulated in reverse, and the row index is unary zero.

    def headerResultTapes (n m : Nat) (rowsBits : List Bool) : Tape → List Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape

  4. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_input line 42
  5. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_archive line 45
  6. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_accumulator line 48
  7. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes_rowIndex line 52
  8. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerTimePolynomial line 56

    Source documentation

    A fixed polynomial in the complete encoded input length.

    noncomputable def headerTimePolynomial : Polynomial Nat :=
…
  9. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerTimePolynomial_eval line 59
  10. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerInTime line 65

    Source documentation

    An actual entry-to-guard trace, valid for any unread row suffix and every finite ambient buffer. No execution premise is supplied by the caller.

    def headerInTime (rowPlan : Plan) (n m : Nat) (rowsBits : List Bool) (ambient : Ambient) :
    StateTransition.EvalsToInTime (TM2.step (program headerPlan rowPlan))
      ⟨some .copyFirst, ((ambient, ()), none),
        headerInputTapes (encodeWords [n, m] ++ rowsBits)⟩
      (some ⟨some .guard, ((ambient, ()), none), headerResultTapes n m rowsBits⟩)
      (headerTimePolynomial.eval (encodeWords [n, m] ++ rowsBits).length) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.program, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerInputTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.guard, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes

  11. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.tableRowsBits line 195

    Source documentation

    The unread graph rows in the actual graph codec.

    def tableRowsBits (table : PCP.GenericGraphTables.Table 64) : List Bool :=
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table

  12. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.tableBits_header_rows line 198
  13. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.tableHeaderInTime line 205

    Source documentation

    Specialization to the entire input of the actual numbered graph codec.

    def tableHeaderInTime (rowPlan : Plan) (table : PCP.GenericGraphTables.Table 64)
    (ambient : Ambient) :
    StateTransition.EvalsToInTime (TM2.step (program headerPlan rowPlan))
      ⟨some .copyFirst, ((ambient, ()), none),
        headerInputTapes (PCP.GenericGraphTables.tableBits table)⟩
      (some ⟨some .guard, ((ambient, ()), none),
        headerResultTapes table.vertices table.darts (tableRowsBits table)⟩)
      (headerTimePolynomial.eval (PCP.GenericGraphTables.tableBits table).length) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.program, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerInputTapes, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.guard, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.tableRowsBits

  14. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerInput_configuration line 216
  15. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.initializedTableHeaderInTime line 226

    Source documentation

    The same bounded phase begins at the machine's genuine initial configuration.

    def initializedTableHeaderInTime (rowPlan : Plan) (table : PCP.GenericGraphTables.Table 64) :
    StateTransition.EvalsToInTime (machine headerPlan rowPlan).step
      (initList (machine headerPlan rowPlan) (PCP.GenericGraphTables.tableBits table))
      (some ⟨some .guard, ((((), fun _ => false), ()), none),
        headerResultTapes table.vertices table.darts (tableRowsBits table)⟩)
      (headerTimePolynomial.eval (PCP.GenericGraphTables.tableBits table).length) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.machine, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.guard, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerResultTapes, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.tableRowsBits

  16. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.endpointTapes line 247
  17. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.endpointsInTime line 254

    Source documentation

    Read the two fields actually stored in a graph row: tail and reverse dart.

    def endpointsInTime (headerPlan plan : Plan) (base : Tape → List Bool)
    (tail reverse : Nat) (rest : List Bool)
    (hinput : base .input = encodeWord tail ++ encodeWord reverse ++ rest)
    (ambient : Ambient) :
    StateTransition.EvalsToInTime (TM2.step (program headerPlan plan))
      ⟨some .startTail, ((ambient, ()), none), base⟩
      (some ⟨some .headTableFirst, ((ambient, ()), none),
        endpointTapes base tail reverse rest⟩) (tail + reverse + 4) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.program, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.endpointTapes

  18. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.relationInTime line 280

    Source documentation

    The fixed unary relation reader occupies one finite TM2 statement.

    def relationInTime (headerPlan plan : Plan) (base : Tape → List Bool)
    (relation : GraphTables.RelationTable) (rest : List Bool)
    (hinput : base .input = encodeWords (GraphTables.relationWords relation) ++ rest)
    (ambient : Ambient) :
    StateTransition.EvalsToInTime (TM2.step (program headerPlan plan))
      ⟨some .readRelation, ((ambient, ()), none), base⟩
      (some ⟨some (.row (Emitter.labelAt plan.length 36864 0 .entry)),
        ((((), fun i => relation[i]), ()), none), Function.update base .input rest⟩) 1 where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.program

  19. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.emitInTime line 295

    Source documentation

    Execute the complete fixed row emission plan against physical unary tapes.

    def emitInTime (headerPlan plan : Plan) (base : Tape → List Bool)
    (operands : Fin 5 → Nat) (hoperands : ∀ i, base (source i) = encodeWord (operands i))
    (hscratch : base .scratch = []) (ambient : Ambient)
    (N : Nat) (hbounded : ∀ i, operands i ≤ N) :
    StateTransition.EvalsToInTime (TM2.step (program headerPlan plan))
      ⟨some (.row (Emitter.labelAt plan.length 36864 0 .entry)),
        ((ambient, ()), none), base⟩
      (some ⟨some .clearTail, ((ambient, ()), none),
        Function.update base .accumulator
          ((plan.flatMap (Emitter.commandBits operands ambient)).reverse ++ base .accumulator)⟩)
      (plan.length * (3 * (N + 1) + 3) + 1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.source, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.program

  20. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.finishTapes line 312
  21. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.finishInTime line 319

    Source documentation

    Clear precisely the three isolated temporary fields and increment the physical row counter before returning to the input guard.

    def finishInTime (headerPlan plan : Plan) (base : Tape → List Bool)
    (tail head reverse row : Nat)
    (htail : base .tail = encodeWord tail) (hhead : base .head = encodeWord head)
    (hreverse : base .reverseIndex = encodeWord reverse)
    (hrow : base .rowIndex = encodeWord row) (ambient : Ambient) :
    StateTransition.EvalsToInTime (TM2.step (program headerPlan plan))
      ⟨some .clearTail, ((ambient, ()), none), base⟩
      (some ⟨some .guard, ((ambient, ()), none), finishTapes base row⟩)
      (tail + head + reverse + 4) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.program, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.guard, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.finishTapes

  22. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow line 369
  23. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_tail line 373
  24. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_reverseIndex line 376
  25. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_relation line 379
  26. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows line 382
  27. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_get line 385
  28. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_reverseAt line 389
  29. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_acceptsAt line 396
  30. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_valid line 403
  31. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable line 412

    Source documentation

    No row is recomputed, reordered, or selected by an abstract enumeration.

    def genericTable (table : GraphTables.Table) : GenericGraphTables.Table 64 where
…
  32. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_vertices line 418
  33. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_darts line 421
  34. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_row line 424
  35. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tail line 427
  36. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_reverseIndex line 432
  37. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_relation line 437
  38. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_words line 442
  39. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_rowList line 445
  40. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tableWords line 451
  41. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tableBits line 458

    Source documentation

    The shared lookup machine consumes exactly the original serialized input.

    @[simp] theorem genericTable_tableBits (table : GraphTables.Table) :
    GenericGraphTables.tableBits (genericTable table) = GraphTables.tableBits table := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable

  42. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_tail line 462
  43. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_reverse line 466
  44. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_head line 471
  45. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_accepts line 477
  46. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headIndex line 482
  47. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headValue line 486
  48. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headValue_tableGraph line 492
  49. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_pattern_relation line 498
  50. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_zero line 513
  51. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_one line 514
  52. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_two line 515
  53. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_three line 516
  54. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_four line 517
  55. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_five line 518
  56. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowOperands line 520
  57. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowRelation line 524
  58. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowRest line 527
  59. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.preparedTapes line 530
  60. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_input line 536
  61. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_head line 542
  62. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_tail line 550
  63. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_reverse line 556
  64. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_frame line 563
  65. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.emittedTapes line 571
  66. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResultTapes line 577
  67. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_input line 581
  68. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_tail line 586
  69. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_head line 591
  70. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_reverse line 596
  71. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_index line 601
  72. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_accumulator line 606
  73. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowResult_frame line 613
  74. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.guardRowInTime line 624
  75. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.guardEndInTime line 637
  76. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.prepared_operands line 650

    Source documentation

    All five unbounded operands remain isolated encoded naturals after the row parser and head lookup, including both independently retrieved endpoints.

    theorem prepared_operands (base : Tape → List Bool) (table : GraphTables.Table)
    (e : Fin table.darts) (rest : List Bool)
    (hn : base .vertices = encodeWord table.vertices)
    (hm : base .darts = encodeWord table.darts)
    (hr : base .rowIndex = encodeWord e.val)
    (ht : base .tail = []) :
    ∀ i, (Function.update (preparedTapes base table e rest) Tape.input rest) (source i) =
      encodeWord (rowOperands table e i) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.preparedTapes, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.source, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowOperands

  77. theorem OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowOperands_bounded line 679
  78. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowTime line 690
  79. def OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowInTime line 696

    Source documentation

    Run one complete stored row, including the actual table-based head lookup. The only hypotheses describe the physical input tapes; no execution or serialization correctness of a caller-provided body is assumed.

    noncomputable def rowInTime (headerPlan plan : Plan) (base : Tape → List Bool)
    (table : GraphTables.Table) (e : Fin table.darts) (rest : List Bool)
    (hinput : base .input = encodeWords (GraphTables.rowWords table.rows[e]) ++ rest)
    (harchive : base .archive = GraphTables.tableBits table)
    (hn : base .vertices = encodeWord table.vertices)
    (hm : base .darts = encodeWord table.darts)
    (hrow : base .rowIndex = encodeWord e.val)
    (ht : base .tail = []) (hh : base .head = []) (hr : base .reverseIndex = [])
    (hscratch : base .scratch = []) (ambient : Ambient) :
    StateTransition.EvalsToInTime (TM2.step (program headerPlan plan))
      ⟨some .startTail, ((ambient, ()), none), base⟩
      (some ⟨some .guard, ((rowRelation table e, ()), none),
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Plan, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Tape, OAI.MaxCutGames.Foundations.Complexity.encodeWords, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.program, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.guard, OAI.MaxCutGames.Foundations.Complexity.FinalCNFMachine.Program.rowRelation