proposition: Lemma While_merge_term k1 (c1 c2 : mconfig sig (state WhileTM) n) (f : F) : loopM (projT1 pM) c1 k1 = Some c2 -> (projT2 pM) (cstate c2) = Some f -> loopM WhileTM c1 k1 = Some c2.
proof: Proof. intros HLoop HTerm. unfold loopM in *. eapply loop_lift with (lift := id) (f' := step (WhileTM)) (h' := haltConf (M := projT1 pM)) in HLoop; cbv [id] in *; cbn; auto; cycle 1. { intros. symmetry. now apply step_comp. } unfold loopM. replace k1 with (k1 + 0) by lia. apply loop_merge with (h := haltConf (M := projT1 pM)) (a2 := c2). - apply halt_comp. - apply HLoop. - cbn in *. setoid_rewrite (loop_fulfills HLoop). rewrite HTerm. cbn. reflexivity. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts