proposition: Lemma Nop_Sem : Nop ⊨c(0) Nop_Rel.
proof: Proof. intros t. cbn. unfold initc; cbn. eexists (mk_mconfig _ _); cbn; eauto. Qed.
imports: Undecidability(TM.Util.Prelim) Undecidability(TM.Util.TM_facts) Undecidability(TM.Basic.Mono) Undecidability(TM.Combinators.Combinators) Undecidability(TM.Compound.TMTac)