proposition: Lemma StateWhile_split_repeat k l l1 c2 c3 : loop (step (StateWhileTM l)) (haltConf (M:=StateWhileTM l)) (lift c2) k = Some c3 -> haltConf c2 = true -> projT2 (pM l) (cstate c2) = inl l1 -> exists k', loop (step (StateWhileTM l)) (haltConf (M:=StateWhileTM l)) (lift (initc (projT1 (pM l1)) (ctapes c2))) k' = Some c3 /\ k = S k'.
proof: Proof. intros HLoop H E. unfold haltConf in H. destruct k as [ |k']; cbn in *; unfold StateWhile_halt in *; cbn in *. - rewrite H, E in HLoop. cbn in *. congruence. - rewrite H, E in HLoop. cbn in *. exists k'. repeat split; auto. rewrite <- HLoop. f_equal. symmetry. apply StateWhile_trans_repeat; auto. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts