OAI/NumberTheory/Ostmann/Construction/ExpandedScheduleRanges.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.ScheduleAtomRange line 12
2. def OAI.Ostmann.ScheduleAtomRange.Holds line 17
3. def OAI.Ostmann.ScheduleAtomRange.toWord line 21
4. theorem OAI.Ostmann.ScheduleAtomRange.toWord_holds line 25
5. theorem OAI.Ostmann.ScheduleAtomRange.toWord_length line 32
6. def OAI.Ostmann.expandedScheduleRanges line 39
7. theorem OAI.Ostmann.expandedScheduleRanges_count_bounded line 50

   Source documentation

   The range count is controlled at every stage, including the terminal bins.

   theorem expandedScheduleRanges_count_bounded {I σ : Type*} (role : I → CopyScheduleRole)
       (address : ℕ → List Bool → σ) (ranges : (n : ℕ) → List (ScheduleAtomRange role n))
       (n K : ℕ) (hK : ∀ j ≤ n, (ranges j).length ≤ K)
       (path : List Bool) (current : CopyScheduleAtoms role n → List σ) :
       (expandedScheduleRanges role address ranges n path current).CountBounded K := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.expandedScheduleRanges

8. theorem OAI.Ostmann.expandedScheduleRanges_words_bounded line 64

   Source documentation

   Products in all original range tests have the same finite word bound as their actual constituent expansion.

   theorem expandedScheduleRanges_words_bounded {I σ : Type*} (role : I → CopyScheduleRole)
       (address : ℕ → List Bool → σ) (ranges : (n : ℕ) → List (ScheduleAtomRange role n))
       (n A M : ℕ) (hM : 1 ≤ M)
       (hA : ∀ j ≤ n, ∀ r ∈ ranges j, r.atoms.length ≤ A)
       (path : List Bool) (current : CopyScheduleAtoms role n → List σ)
       (hc : ∀ i, (current i).length ≤ M) :
       (expandedScheduleRanges role address ranges n path current).WordsBounded (A * M + 1) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.expandedScheduleRanges