proposition: Lemma While_trans_repeat (c : mconfig sig (state WhileTM) n) : haltConf (M := projT1 pM) c = true -> projT2 pM (cstate c) = None -> step WhileTM c = initc (WhileTM) (ctapes c).
proof: Proof. intros HHalt HRepeat. unfold haltConf in HHalt. destruct c as [q t]; cbn in *. unfold step. cbn -[doAct_multi] in *. rewrite HHalt. unfold initc. f_equal. apply doAct_nop. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts