fact: Definition mirrorConf : mconfig sig (state (projT1 pM)) n -> mconfig sig (state (projT1 pM)) n := fun c => mk_mconfig (cstate c) (mirror_tapes (ctapes c)).
imports: Undecidability(TM.Util.Prelim TM.Util.TM_facts)