proposition: Theorem ra_min_extra : ex (⟦ra_min f⟧ v) <-> exists x, ⟦f⟧ (x##v) 0.
proof: Proof. Proof using Hf. split. + intros (x & H1 & H2); exists x; auto. + intros (x & Hx). destruct bounded_min_d with (P := fun x => ⟦f⟧ (x##v) 0) (Q := fun x => exists k, ⟦f⟧ (x##v) (S k)) (n := S x) as [ (m & H1 & H2 & H3) | H1 ]; auto. * intros y _; destruct (Hf y) as ([ | k ] & Hk); auto. right; exists k; auto. * exists m; split; auto. * destruct (H1 _ (Nat.le_refl _)) as (k & Hk). generalize (ra_rel_fun _ _ _ _ Hx Hk); discriminate. Qed.
imports: Arith Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_decidable pos vec) Undecidability.MuRec.Util(recalg ra_utils)