proposition: Lemma Mirror_Terminates T : projT1 pM ↓ T -> projT1 Mirror ↓ Mirror_T T.
proof: Proof. intros HTerm. hnf. intros t1 k H1. hnf in HTerm. specialize (HTerm (mirror_tapes t1) k H1) as (outc&H). exists (mirrorConf outc). apply mirror_unlift. cbn. now rewrite mirrorConf_involution. Qed.
imports: Undecidability(TM.Util.Prelim TM.Util.TM_facts)