proposition: Lemma StateWhile_merge_repeat k1 k2 l l1 (c1 : mconfig sig (state (projT1 (pM l))) n) (c2 : mconfig sig (state (projT1 (pM l))) n) c3 : loopM (projT1 (pM l)) c1 k1 = Some c2 -> haltConf c2 = true -> projT2 (pM l) (cstate c2) = inl l1 -> loopM (StateWhileTM l) (lift (initc (projT1 (pM l1)) (ctapes c2))) k2 = Some c3 -> loopM (StateWhileTM l) (lift c1) (k1 + (1 + k2)) = Some c3.
proof: Proof. intros HLoop1 HHalt HL HLoop2. unfold loopM in *. apply loop_merge with (f := step (StateWhileTM l)) (h := @lifth l) (a2 := lift c2). - apply lifth_comp. - eapply loop_lift. 3: apply HLoop1. 2: eauto. + apply lifth_comp'. + apply step_comp. - cbn [plus]. rewrite loop_step. + now rewrite StateWhile_trans_repeat with (l' := l1). + cbn; unfold StateWhile_halt; cbn. rewrite HL. apply andb_false_r. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts