proposition: Lemma Switch_split k t (outc : mconfig sig (state SwitchTM) n) : loopM (initc SwitchTM t) k = Some outc -> exists k1 (c1 : mconfig sig (state M1) n) k2 (c2 : mconfig sig (state (Mf (p1 (cstate c1)))) n), loopM (initc M1 t) k1 = Some c1 /\ loopM (initc (Mf (p1 (cstate c1))) (ctapes c1)) k2 = Some c2 /\ outc = lift_confR c2.
proof: Proof. unfold loopM. intros H. apply loop_split with (h := halt_liftL) in H as (k1&c1&k2&HLoop1&HLoop2&_). - rewrite lift_initc in HLoop1. apply loop_unlift with (lift := lift_confL) (f := step (M := M1)) (h := haltConf (M := M1)) in HLoop1 as (c1'&HLoop1&->). + apply step_nop_split in HLoop2 as (k2'&c2'&_&HLoop2&->). 2: now apply (loop_fulfills HLoop1). exists k1, c1', k2', c2'. auto. + intros. cbn. reflexivity. + intros. now apply step_comp_liftL. - apply halt_conf_liftL. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts