OAI/Combinatorics/LowSpaceSubsetSum/Streams/PrefixTaskCount.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LowSpaceSubsetSum.RepresentationParentData.overflowCount line 14
2. def OAI.LowSpaceSubsetSum.RepresentationParentData.taskStarts line 22
3. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.taskStarts_le_overflow line 29
4. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.entryUniverse_force_card_add line 45
5. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.overflowCount_capacity line 57
6. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.taskStarts_capacity line 90
7. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.completedArrays_length_le line 102
8. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.completedArrays_size_sum_le line 120
9. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.input_sum line 150
10. theorem OAI.LowSpaceSubsetSum.RepresentationParentData.completed_check_inputs_le line 160

    Source documentation

    Includes every reuse of the retained left array at a completed right prefix; it is the actual check list's input-occurrence bound.

    theorem completed_check_inputs_le (B L : ℕ) (hL : L ≤ D.capacity)
        (hd : ∀ i j, i ≠ j → Disjoint (D.leaves i).top (D.leaves j).top)
        (hbounded : ∀ P, ∀ e ∈ ({ D with maskRestriction := P }).rawEntries,
    …

    Mentions: OAI.LowSpaceSubsetSum.RepresentationParentData.rawEntries