proposition: Lemma loop_merge (k1 k2 : nat) (a1 a2 a3 : A) : loop f h a1 k1 = Some a2 -> loop f h' a2 k2 = Some a3 -> loop f h' a1 (k1+k2) = Some a3.
proof: Proof. Proof using halt_comp. revert a1 a2 a3. induction k1 as [ | k1' IH]; intros a1 a2 a3 HLoop1 HLoop2; cbn in HLoop1. - now destruct (h a1); inv HLoop1. - destruct (h a1) eqn:E. + inv HLoop1. eapply loop_monotone; eauto. lia. + cbn. rewrite (halt_comp E). eapply IH; eauto. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes Undecidability.Shared.Libs.PSL.FiniteTypes.BasicFinTypes Undecidability.Shared.Libs.PSL.FiniteTypes.CompoundFinTypes Undecidability.Shared.Libs.PSL.FiniteTypes.VectorFin Undecidability.Shared.Libs.PSL.Vectors.FinNotation Undecidability.Shared.Libs.PSL.Inhabited Undecidability.Shared.Libs.PSL.Base Undecidability.Shared.Libs.PSL.Vectors.Vectors Lia