The Adian--Rabin family obtained from the compressed Miller--Tancer construction.

def Undecidability.MillerTancer.Compressed.family {n m : ℕ} (P : FP n m) (k : Fin n) : ℕ → FP (n + 1) (m + 2)

Natural-number-indexed compressed Miller--Tancer family.

Equations

• Undecidability.MillerTancer.Compressed.family P k j = Undecidability.MillerTancer.Compressed.transform P k (Undecidability.wordOfNat n j)

theorem Undecidability.MillerTancer.Compressed.family_isAdianRabin {n m : ℕ} (P : FP n m) (k : Fin n) (hP : ¬ComputablePred P.wordProblem) (hk : P.NormallyGenerates (Word.generator k)) : FP.IsAdianRabinFamily (family P k)

The compressed family is an effective Adian--Rabin family.