proposition: Lemma StateWhile_split k l (c1 : mconfig sig (state (projT1 (pM l))) n) (c3 : mconfig sig (FinType (EqType StateWhile_states)) n) : loopM (StateWhileTM l) (lift c1) k = Some c3 -> exists (c2 : mconfig sig (state (projT1 (pM l))) n), match projT2 (pM l) (cstate c2) with | inl l1 => exists (k1 k2 : nat), loopM (projT1 (pM l)) c1 k1 = Some c2 /\ loopM (StateWhileTM l) (lift (initc (projT1 (pM l1)) (ctapes c2))) k2 = Some c3 /\ 1 + k1 + k2 <= k | inr l2 => loopM (projT1 (pM l)) c1 k = Some c2 /\ c3 = lift c2 end.
proof: Proof. intros HLoop. unfold loopM in *. apply loop_split with (h := @lifth l) in HLoop as (k1&c2&k2&HLoop1&HLoop2&Hk). - apply loop_unlift with (f := step (projT1 (pM l))) (h := haltConf (M := projT1 (pM l))) in HLoop1 as (c2'&HLoop1&->). + exists c2'. destruct (projT2 (pM l) (cstate c2')) as [l1|l2] eqn:E. * exists k1. eapply StateWhile_split_repeat in HLoop2 as (k2'&HLoop2&->). -- exists k2'. repeat split. all: eauto. lia. -- now apply loop_fulfills in HLoop1. -- easy. * split. -- eapply loop_monotone. ++ apply HLoop1. ++ lia. -- eapply StateWhile_split_break; eauto. now apply loop_fulfills in HLoop1. + apply lifth_comp'. + apply step_comp. - apply lifth_comp. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts