proposition: Lemma While_split k (c1 c3 : mconfig sig (state (projT1 pM)) n) : loopM WhileTM c1 k = Some c3 -> exists k1 k2 c2, loopM (projT1 pM) c1 k1 = Some c2 /\ loopM WhileTM c2 k2 = Some c3 /\ k1 + k2 <= k.
proof: Proof. unfold loopM. intros HLoop. apply loop_split with (h := haltConf (M := projT1 pM)) in HLoop as (k1&c2&k2&HLoop&HLoop'&Hk). - exists k1, k2, c2. repeat split; eauto. apply loop_lift with (lift := id) (f' := step (projT1 pM)) (h' := haltConf (M := projT1 pM)) in HLoop. + apply HLoop. + auto. + apply step_comp. - apply halt_comp. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts