proposition: Lemma config_enumeration (M : SBTM) : { e : nat -> option (config M) | enumerator__T e (config M) }.
proof: Proof. eexists. apply enumerator__T_prod. + apply enumerator__T_Fin. + apply enumerator__T_prod; [apply enumerator__T_prod|]. * eapply ListEnumerabilityFacts.enumerator__T_to_list. eapply ListEnumerabilityFacts.enumerator__T_list. eapply ListEnumerabilityFacts.enumerator__T_of_list. apply enumerator__T_bool. * apply enumerator__T_bool. * eapply ListEnumerabilityFacts.enumerator__T_to_list. eapply ListEnumerabilityFacts.enumerator__T_list. eapply ListEnumerabilityFacts.enumerator__T_of_list. apply enumerator__T_bool. Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts) Undecidability.TM.SBTM