proposition: Lemma ra_bs_inc_rel k (f : recalg k) v x : [f;v] ▹ x -> [|f|] v x.
proof: Proof. induction 1 as [ n v | v | v | k v p | k i f gj v w x H1 IH1 H2 | k f g v n x H1 | k f g v n x y H1 IH1 H2 | k f v n w H1 IH1 H2 ]; try reflexivity. exists w; split; auto; intros; rewrite vec_pos_set; auto. red; unfold s_rec; simpl; auto. rewrite ra_rel_fix_rec in IH1 |- *; unfold s_rec in IH1 |- *. simpl in IH1 |- *; exists x; auto. rewrite ra_rel_fix_min; unfold s_min; split; auto. intros y Hy. exists (vec_pos w (nat2pos Hy)). generalize (IH1 (nat2pos Hy)). rewrite pos2nat_nat2pos. eqgoal; do 2 f_equal. Qed.
imports: Undecidability.Shared.Libs.DLW(utils finite pos vec) Undecidability.MuRec.Util(recalg recursor minimizer ra_ca)