From c57405141d26ac2215a07b05d27a16a691dda50e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 26 Mar 2010 18:14:54 +0000 Subject: [PATCH] Good definition found. From: sacerdot --- helm/software/matita/nlibrary/arithmetics/R.ma | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma index 9087304bd..046bcbf88 100644 --- a/helm/software/matita/nlibrary/arithmetics/R.ma +++ b/helm/software/matita/nlibrary/arithmetics/R.ma @@ -169,16 +169,14 @@ nqed. ncoinductive ftfish (A : Ax_pro) (F : Ω^A) : A → CProp[0] ≝ | ftfish : ∀a. a ∈ F → - (*(∀i:𝐈 a .∃b. b ∈ 𝐂 a i ∧ ftfish A F b) →*) (∀b. a ≤ b → ftfish A F b) → - (∀b. a ≤ b → ∀i:𝐈 b. ∃x. x ∈ 𝐂 b i ↓ (singleton … a) ∧ ftcover A F x) → + (∀b. a ≤ b → ∀i:𝐈 b. ∃x. x ∈ 𝐂 b i ↓ (singleton … a) ∧ ftfish A F x) → ftfish A F a. -ntheorem - -interpretation "fish" 'fish a U = (fish ? U a). +interpretation "fish" 'fish a U = (ftfish ? U a). alias symbol "I" (instance 6) = "I". ntheorem ftcoinfinity: ∀A: Ax_pro. ∀F: Ω^A. ∀a. a ⋉ F → (∀i: 𝐈 a. ∃b. b ∈ 𝐂 a i ∧ b ⋉ F). - #A; #F; #a; *; #b; #H; #H1; #i; @ a; @; //; - ncases H; \ No newline at end of file + #A; #F; #a; #H; ncases H; #b; #_; #_; #H2; #i; ncases (H2 … i); //; + #x; *; *; *; #y; *; #K2; #K3; #_; #K5; @y; @ K2; ncases K5 in K3; /2/. +nqed. \ No newline at end of file -- 2.39.2