proposition: Lemma Switch_merge t (k1 k2 : nat) (c1 : mconfig sig (state M1) n) (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 -> loopM (initc SwitchTM t) (k1 + (1 + k2)) = Some (lift_confR c2).
proof: Proof. intros HLoop1 HLoop2. unfold loopM in *. apply loop_merge with (h := halt_liftL) (a2 := lift_confL c1). - apply halt_conf_liftL. - rewrite lift_initc. apply loop_lift with (h := haltConf (M := M1)) (f := step (M := M1)). + unfold haltConf. intros. cbn. reflexivity. + apply step_comp_liftL. + apply HLoop1. - rewrite loop_step by auto. rewrite step_nop_transition by apply (loop_fulfills HLoop1). eapply loop_lift with (lift := lift_confR (f := p1 (cstate c1))) (f' := step (M := SwitchTM)) (h' := haltConf (M := SwitchTM)) in HLoop2. + apply HLoop2. + intros. cbn. now destruct x. + intros. apply step_comp_liftR. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts