PredecessorWordEquivalence.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite predecessor words encode the same past as the countable observation

theorem OAI.DukePrimeDegree.predecessor_word_eq_iff line 13

Source documentation

Given the terminal symbol, the finite predecessor labels recover the whole countable word, and conversely.

theorem predecessor_word_eq_iff {Y A : Type*} (T : Y → Y) (Q : Y → ℕ)
    (B : Y → A)
    (href : ∀ x y, Q x=Q y → Q (T x)=Q (T y) → B x=B y)
    (decode : ℕ → A → ℕ) (hdecode : ∀ x, decode (Q (T x)) (B x)=Q x)
    (N : ℕ) (x y : Y) (ht : Q (T^[N] x)=Q (T^[N] y)) :
    orbitName T Q N x=orbitName T Q N y ↔
      orbitName T B N x=orbitName T B N y := by
…