proposition: Lemma While_split_term k (c1 c2 : mconfig sig (state WhileTM) n) (f : F) : loopM WhileTM c1 k = Some c2 -> haltConf (M := projT1 pM) c1 = true -> projT2 pM (cstate c1) = Some f -> c2 = c1.
proof: Proof. intros HLoop HHalt HTerm. unfold loopM in *. eapply loop_eq_0. 2: apply HLoop. unfold haltConf in *. cbn in *. now rewrite HHalt, HTerm. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts