OAI/NumberTheory/Ostmann/Construction/WordTransferGuardReplay.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.WordTransferTemplate.guards line 11
2. theorem OAI.Ostmann.wordTransferUpdatedFormulas_nat line 21
3. theorem OAI.Ostmann.WordTransferTemplate.guards_iff line 39

   Source documentation

   The list contains precisely the original support conditions at every node, including the independent substitutions on the two child branches.

   theorem WordTransferTemplate.guards_iff {σ : Type*} {n : ℕ}
       (template : WordTransferTemplate σ n) (t : FrequencyTree ℤ n)
       (hn : NonzeroInternalFrequencies n t) (env : σ → HistoryFormula σ)
       (a : σ → ℤ) (x : σ → ℕ)
       (henv : ∀ i, (env i).value (fun j => (a j : ℚ)) = (x i : ℚ)) :
       (∀ g ∈ template.guards t hn env, g.ValidAt a) ↔
         ValidTransferHistory (wordTransferSystem σ) n (template.state x) t := by
   …

   Mentions: OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.HistoryFormula, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.wordTransferSystem

4. theorem OAI.Ostmann.WordTransferTemplate.guards_length line 63
5. theorem OAI.Ostmann.WordTransferTemplate.guards_pivots line 74