ConstituentScheduleMap.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Forgetting constituent indices commutes with the literal copy schedule

def OAI.Ostmann.copyScheduleMap line 10

Source documentation

Apply a map of original labels without changing any copy/retain choice.

def copyScheduleMap {I J : Type*} (f : I → J) :
    (n : ℕ) → CopyScheduleVertex I n → CopyScheduleVertex J n
  | 0, i => f i
  | n + 1, .inl (b, i) => .inl (b, copyScheduleMap f n i)
  | n + 1, .inr i => .inr (copyScheduleMap f n i)

Mentions: OAI.Ostmann.CopyScheduleVertex

theorem OAI.Ostmann.copyScheduleOrigin_map line 16
theorem OAI.Ostmann.copyScheduleMap_positive line 24
theorem OAI.Ostmann.copyScheduleMap_path line 30
theorem OAI.Ostmann.copyScheduleRole_map line 37
theorem OAI.Ostmann.copyScheduleSurvives_map_iff line 48
Source documentation
The prime constituents of an atom survive precisely when the atom does.
```
theorem copyScheduleSurvives_map_iff {I J : Type*} (f : I → J)
    (role : J → CopyScheduleRole) (n : ℕ) (i : CopyScheduleVertex I n) :
    CopyScheduleSurvives role n (copyScheduleMap f n i) ↔
      CopyScheduleSurvives (role ∘ f) n i := by
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.CopyScheduleSurvives, OAI.Ostmann.copyScheduleMap