proposition: Lemma StateWhile_merge_break k l l2 (c1 : mconfig sig (state (projT1 (pM l))) n) (c2 : mconfig sig (state (projT1 (pM l))) n) : loopM (projT1 (pM l)) c1 k = Some c2 -> haltConf c2 = true -> projT2 (pM l) (cstate c2) = inr l2 -> loopM (StateWhileTM l) (lift c1) k = Some (lift c2).
proof: Proof. intros HLoop HHalt HL. unfold loopM in *. replace k with (k + 0) by lia. apply loop_merge with (f := step (StateWhileTM l)) (h := @lifth l) (a2 := lift c2). - apply lifth_comp. - eapply loop_lift with (lift := lift) (f' := step (StateWhileTM l)) (h' := @lifth l) in HLoop; auto. + apply lifth_comp'. + apply step_comp. - cbn. unfold StateWhile_halt; cbn. unfold haltConf in *. rewrite HHalt, HL. cbn. reflexivity. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts