proposition: Fact ra_dio_poly_test_prim : prim_rec ra_dio_poly_test.
proof: Proof. simpl; split; auto. intros i. rewrite vec_pos_set. destruct (pos_both n m i). + simpl; split; auto. intros j; analyse pos j; simpl; auto. + simpl; auto. Qed.
imports: List Arith Undecidability.Shared.Libs.DLW(utils_tac utils_nat pos vec) Undecidability.MuRec.Util(recalg ra_utils recomp ra_recomp) Undecidability.H10.Dio(dio_single)