proposition: Lemma ra_bs_to_c k (f : recalg k) v x : [ f; v ] ▹ x -> exists c, [f ; v ; 0 ; c] ▹ x.
proof: Proof. induction 1. - exists 1. econstructor. - exists 1. econstructor. - exists 1. econstructor. - exists 1. econstructor. - destruct IHra_bs as [c]. eapply vec_reif in H0 as [cst]. exists (2 + c + vec_sum cst + k). cbn. econstructor. + intros. eapply ra_bs_mono. 1:eauto. rewrite <- Nat.add_sub_assoc. 2: pose (pos2nat_prop j); lia. enough (vec_pos cst j <= vec_sum cst). 1: lia. eapply vec_sum_le. + eapply ra_bs_mono. 1: eauto. lia. - destruct IHra_bs as [c]. exists (S c). now econstructor. - destruct IHra_bs1 as [c1]. destruct IHra_bs2 as [c2]. exists (1 + c1 + c2). cbn. econstructor. + eapply ra_bs_mono. 1: eauto. lia. + eapply ra_bs_mono. 1: eauto. lia. - destruct IHra_bs as [c]. eapply vec_reif in H0 as [cst]. exists (1 + c + vec_sum cst + x). cbn. econstructor. 1: lia. + intros. eapply ra_bs_mono. 1: eauto. rewrite <- Nat.add_sub_assoc. 2: pose (pos2nat_prop j); lia. enough (vec_pos cst j <= vec_sum cst) by lia. eapply vec_sum_le. + eapply ra_bs_mono. 1: eauto. lia. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.L.Datatypes(LNat LOptions LSum) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared(DLW.Utils.finite DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec(MuRec recalg ra_sem_eq)