Existence

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

theorem Undecidability.Host.exists_threeNineHost : ∃ (P : FP 3 9), (∃ (z : Word 3), P.NormallyGenerates z) ∧ ¬ComputablePred P.wordProblem

A three-generator, nine-relator host with the extra normal-weight-one property.