Tower

Part of the dependency closure of the small undecidable group constructions.

theorem Undecidability.Host.borisov_testWord_iff_compressed (datum : Thue.StandingDatum) (Q : List (Fin 2)) : (Borisov.presentation datum).wordProblem (Borisov.testWord Q) ↔ (presentationOf datum).wordProblem (testWord Q)

The two proper HNN embeddings and the six Tietze eliminations preserve the truth of Borisov's test word.

theorem Undecidability.Host.thueEq_iff_testWord (datum : Thue.StandingDatum) (Q : List (Fin 2)) : ThueEq (Thue.systemOf datum.F datum.E) Q datum.P ↔ (presentationOf datum).wordProblem (testWord Q)

The Thue predicate is represented by the compressed host test word.

theorem Undecidability.Host.z_normallyGenerates (datum : Thue.StandingDatum) : (presentationOf datum).NormallyGenerates zWord

Normal generation from Proposition 2.4 of the paper, proved in the compressed presentation.

theorem Undecidability.Host.wordProblem_unsolvable (datum : Thue.StandingDatum) : ¬ComputablePred (presentationOf datum).wordProblem

The explicit compressed host has unsolvable word problem.