OAI/NumberTheory/Ostmann/Construction/InsertedAtomAssignment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledInsertedAtoms line 12
2. theorem OAI.Ostmann.scheduledInsertedAtoms_pivot line 20
3. theorem OAI.Ostmann.scheduledInsertedAtoms_H line 26
4. theorem OAI.Ostmann.scheduledInsertedAtoms_Y line 33
5. theorem OAI.Ostmann.reverseCopiedAtoms_eq_inserted line 42

   Source documentation

   The arithmetic reverse substitution uses precisely the old H branch, the single common outside assignment, and the forced composite pivot.

   theorem reverseCopiedAtoms_eq_inserted {I : Type*} (role : I → CopyScheduleRole)
       (n : ℕ) (b : Bool) (P : ℕ)
       (u : CopyScheduleY role n → ℕ) (l r : CopyScheduleH role n → ℕ) :
       reverseCopyLabelMap role n b P (scheduledCopiedAssignment role n u l r) =
         scheduledInsertedAtoms role n P (if b then l else r) u := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.reverseCopyLabelMap, OAI.Ostmann.scheduledCopiedAssignment, OAI.Ostmann.scheduledInsertedAtoms