proposition: Lemma While_merge_repeat k1 k2 (c1 c2 c3 : mconfig sig (state WhileTM) n) : loopM (projT1 pM) c1 k1 = Some c2 -> (projT2 pM) (cstate c2) = None -> loopM WhileTM (initc WhileTM (ctapes c2)) k2 = Some c3 -> loopM WhileTM c1 (k1+(1+k2)) = Some c3.
proof: Proof. intros HLoop1 HRepeat HLoop2. unfold loopM in *. eapply loop_lift with (lift := id) (f' := step (WhileTM)) (h' := haltConf (M := projT1 pM)) in HLoop1; cbv [id] in *; cbn; auto; cycle 1. { intros. symmetry. now apply step_comp. } apply loop_merge with (h := haltConf (M := projT1 pM)) (a2 := c2). - apply halt_comp. - apply HLoop1. - cbn [loop plus]. rewrite While_trans_repeat; auto. 2: apply (loop_fulfills HLoop1). cbn in *. setoid_rewrite (loop_fulfills HLoop1). now rewrite HRepeat. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts