proposition: Lemma ra_ca_inc_bs k (f : recalg k) v x : (exists n, [f;v] -[n>> x) -> [f;v] ▹ x.
proof: Proof. intros (n & H); revert H. induction 1 as [ n v | v | v | k v p | k i f gj v n w q x H1 IH1 H2 IH2 | k f g v n x H1 IH2 | k f g v n p x q y H1 IH1 H2 IH2 | k f v p n w q H1 IH1 H2 IH2 ]; try (constructor; auto; fail). apply in_ra_bs_comp with w; auto. apply in_ra_bs_rec_S with x; auto. apply in_ra_bs_min with w; auto. Qed.
imports: Undecidability.Shared.Libs.DLW(utils finite pos vec) Undecidability.MuRec.Util(recalg recursor minimizer ra_ca)