SelectedWordReversal.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Reversal keeps unexposed leaf primes out of every outside coordinate

theorem OAI.Ostmann.reverseCopyLabelMap_wordOutside_independent line 10
def OAI.Ostmann.reversedWordOutside line 41

theorem OAI.Ostmann.reverseCopyLabelMap_wordLeaf_assignment line 49

Source documentation

Each child has precisely its own unexposed leaf primes. All other child coordinates are functions of the old outside assignment and the forced pivot.

theorem reverseCopyLabelMap_wordLeaf_assignment {I : Type*}
    (role : I → CopyScheduleRole) (i : I) (hi : role i = .word) (n : ℕ) (b : Bool) (P : ℕ)
    (y : WordLeafOutside role i hi (n + 1) → ℕ) (x : TreeLeafIndex (n + 1) → ℕ) :
    reverseCopyLabelMap role n b P (wordLeafAssignment role i hi (n + 1) y x) =
      wordLeafAssignment role i hi n (reversedWordOutside role i hi n b P y)
        (fun t => x (if b then .inl t else .inr t)) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.WordLeafOutside, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.reverseCopyLabelMap, OAI.Ostmann.wordLeafAssignment, OAI.Ostmann.reversedWordOutside