OAI/NumberTheory/Ostmann/Construction/ScheduleAtomSystem.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.ScheduleAtomState line 11
2. def OAI.Ostmann.scheduleAtomLeft line 14
3. def OAI.Ostmann.scheduleAtomRight line 19
4. def OAI.Ostmann.scheduleAtomBound line 24
5. def OAI.Ostmann.scheduleAtomChild line 29
6. def OAI.Ostmann.scheduleAtomSystem line 34
7. def OAI.Ostmann.expandedAtomValues line 43
8. theorem OAI.Ostmann.expanded_schedule_node_iff line 47
9. theorem OAI.Ostmann.expanded_schedule_child_state line 80

   Source documentation

   The inserted coordinate realizes exactly the original child atom state, with composite atoms evaluated as their constituent prime products.

   theorem expanded_schedule_child_state {I α : Type*} (role : I → CopyScheduleRole)
       (depth n : ℕ) (hn : n ≤ depth) (b : Bool) (path : List Bool)
       (current : CopyScheduleAtoms role (n + 1) → List (ExpandedScheduledVariable α depth))
       (hc : ∀ i v, v ∈ current i → ExpandedCoordinateAfter (n + 1) v)
       (x : ExpandedScheduledVariable α depth → ℕ) (P : ℕ) :
       expandedAtomValues role n
         (reverseCopyLabelMap role n b [expandedPivotAddress α depth n path] current)
         (Function.update x (expandedPivotAddress α depth n path) P) =
         reverseCopyLabelMap role n b P (expandedAtomValues role (n + 1) current x) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ExpandedScheduledVariable, OAI.Ostmann.ExpandedCoordinateAfter, OAI.Ostmann.expandedAtomValues, OAI.Ostmann.reverseCopyLabelMap, OAI.Ostmann.expandedPivotAddress