fact: Definition SwitchTM : TM sig n := {| trans := Switch_trans; halt := Switch_halt; start := inl (start M1); |}.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts