proposition: Lemma step_nop_split (k2 : nat) (c2 : mconfig sig (state M1) n) (outc : mconfig sig (state SwitchTM) n) : haltConf c2 = true -> loopM (M := SwitchTM) (lift_confL c2) k2 = Some outc -> exists k2' c2', k2 = S k2' /\ loopM (M := Mf (p1 (cstate c2))) (initc _ (ctapes c2)) k2' = Some c2' /\ outc = lift_confR c2'.
proof: Proof. unfold loopM. intros HHalt HLoop2. unfold haltConf in HHalt. destruct k2 as [ | k2']. - inv HLoop2. - exists k2'. cbn in HLoop2. rewrite step_nop_transition in HLoop2 by assumption. apply loop_unlift with (f := step (M := Mf (p1 (cstate c2)))) (h := haltConf (M := Mf (p1 (cstate c2)))) in HLoop2 as (c2'&HLoop2&->). + exists c2'. repeat split. exact HLoop2. + intros. reflexivity. + intros. apply step_comp_liftR. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts