ReverseAtomSources.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Ostmann.reverseAtomSource line 12
Source documentation
None is the newly reconstructed pivot. Every other atom reads one particular copied or retained atom from the parent assignment.
```
noncomputable def reverseAtomSource {I : Type*} (role : I → CopyScheduleRole)
    (n : ℕ) (b : Bool) : CopyScheduleAtoms role n → Option (CopyScheduleAtoms role (n + 1)) :=
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms
theorem OAI.Ostmann.reverseAtomSource_pivot line 16
theorem OAI.Ostmann.reverseAtomSource_H line 22
theorem OAI.Ostmann.reverseAtomSource_Y line 28
theorem OAI.Ostmann.reverseAtomSource_injective line 36
Source documentation
A unique pivot atom prevents any duplication in a reverse substitution. In particular each previously inserted pivot occurs at most once in a branch.
```
theorem reverseAtomSource_injective {I : Type*} (role : I → CopyScheduleRole)
    (n : ℕ) (b : Bool)
    (hu : ∀ i j, role i = .pivot n → role j = .pivot n → i = j) :
    Function.Injective (reverseAtomSource role n b) := by
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.reverseAtomSource
theorem OAI.Ostmann.reverseCopyLabelMap_source line 68
theorem OAI.Ostmann.reverseCopyLabelMap_injective line 75