proposition: Theorem min_principle_realizer : forall (f : nat -> nat) (tf : term), (forall e, tf↓e ⊩ ∀₁n∈ℕ, ℕ (f n)) -> forall start e, (min_principle tf start)↓e ⊩ ∃₁n∈ℕ, ∀₁m∈ℕ, f(n) ≤ f(m).
proof: Proof. Ksolve. unfold min_rec. Ksolve. apply (Y_realizer (well_founded_ltof nat f)). unfold ltof. exists (fun n => {Z.of_nat n} → ∃₁n∈ℕ, ∀₁m∈ℕ, f(n) ≤ f(m)). Ksolve. start. apply Ht1. find. Ksolve. apply H. find. start. apply H. find. start. apply ℤle_realizer2. find. find. find. rewrite mapsto_equiv. intro. apply prop_realizer1. omega. Ksolve. omega. Qed.
imports: ZArith ClassicalRealizability.Kbase