OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationJoinCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Live cells of the complete prepaid parent join

The stopped driver keeps a single current state. Each iteration includes its concrete reader, key, tie-buffer, snapshot and dictionary trace. Immutable leaf arrays are retained once by the outer wrapper.

  1. def OAI.LowSpaceSubsetSum.RepresentationJoinCells.run line 19
  2. theorem OAI.LowSpaceSubsetSum.RepresentationJoinCells.run_value line 27
  3. theorem OAI.LowSpaceSubsetSum.RepresentationJoinCells.scale line 51
  4. theorem OAI.LowSpaceSubsetSum.RepresentationJoinCells.run_cells line 64
  5. def OAI.LowSpaceSubsetSum.RepresentationJoinCells.parent line 80
  6. theorem OAI.LowSpaceSubsetSum.RepresentationJoinCells.parent_value line 88
  7. theorem OAI.LowSpaceSubsetSum.RepresentationJoinCells.parent_cells line 96
  8. def OAI.LowSpaceSubsetSum.RepresentationJoinCells.withArrays line 106

    Source documentation

    Explicitly shared arrays are retained once throughout the stopped execution.

    def withArrays (I : Instance n) (F : IndexedMask n) (P t : ℤ) (C B : ℕ)
    (left₁ right₁ left₂ right₂ : Array (LeafRecord n)) {d₁ d₂ : ℕ}
    (fuel₁ fuel₂ control : ℕ) (s₁ : RepresentationGroupCells.Left I F P right₁ d₁)
    (s₂ : RepresentationGroupCells.Right I F P t right₂ d₂) (budget : ℕ) :=
…

    Mentions: OAI.LowSpaceSubsetSum.Instance, OAI.LowSpaceSubsetSum.IndexedMask, OAI.LowSpaceSubsetSum.LeafRecord, OAI.LowSpaceSubsetSum.RepresentationGroupCells.Left, OAI.LowSpaceSubsetSum.RepresentationGroupCells.Right

  9. theorem OAI.LowSpaceSubsetSum.RepresentationJoinCells.withArrays_cells line 113