proposition: Lemma While_split_repeat k (c1 c2 : mconfig sig (state WhileTM) n) : loopM WhileTM c1 k = Some c2 -> haltConf (M := projT1 pM) c1 = true -> projT2 pM (cstate c1) = None -> exists k' : nat, k = S k' /\ loopM WhileTM (initc WhileTM (ctapes c1)) k' = Some c2.
proof: Proof. intros HLoop HHalt HRepeat. unfold haltConf in HHalt. destruct k as [ | k']; cbn in *. - rewrite HHalt, HRepeat in HLoop. cbn in HLoop. inv HLoop. - rewrite HHalt, HRepeat in HLoop. cbn in HLoop. exists k'. split; [reflexivity|]. now rewrite While_trans_repeat in HLoop by auto. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts