proposition: Lemma loop_split (k : nat) (a1 a3 : A) : loop f h' a1 k = Some a3 -> exists k1 a2 k2, loop f h a1 k1 = Some a2 /\ loop f h' a2 k2 = Some a3 /\ k1 + k2 <= k.
proof: Proof. Proof using halt_comp. revert a1 a3. revert k; refine (@size_induction _ id _ _); intros k IH. intros a1 a3 HLoop. cbv [id] in *. destruct k as [ | k']; cbn in *. - destruct (h' a1) eqn:E; inv HLoop. exists 0, a3, 0. cbn. rewrite E. destruct (h a3) eqn:E'. + auto. + apply halt_comp in E'. congruence. - destruct (h a1) eqn:E. + exists 0, a1, (S k'). cbn. rewrite E. auto. + rewrite (halt_comp E) in HLoop. apply IH in HLoop as (k1&c2&k2&IH1&IH2&IH3); [ | lia]. exists (S k1), c2, k2. cbn. rewrite E. repeat split; auto. lia. 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