--- a/src/OrdUtil.agda	Tue Mar 01 15:33:05 2022 +0900
+++ b/src/OrdUtil.agda	Fri Mar 04 19:04:08 2022 +0900
@@ -35,6 +35,12 @@
 o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl
 o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl
 
+¬≡o∅< :  { ox : Ordinal } → ¬ (ox ≡  o∅ )  →  o∅ o< ox  
+¬≡o∅< {ox} not with trio< o∅  ox
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a b ¬c = ⊥-elim ( not (sym b) )
+... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+
 osuc-< :  { x y : Ordinal  } → y o< osuc x  → x o< y → ⊥
 osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox
 osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y

--- a/src/filter.agda	Tue Mar 01 15:33:05 2022 +0900
+++ b/src/filter.agda	Fri Mar 04 19:04:08 2022 +0900
@@ -143,53 +143,8 @@
 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
 prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
 
-----
---
--- Filter/Ideal without ZF 
---     L have to be a Latice
---
-
-record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
-   field
-       filter : L → Set n
-       f⊆P :  PL filter 
-       filter1 : { p q : L } → PL (λ x → q ⊆ x )  → filter p →  p ⊆ q  → filter q
-       filter2 : { p q : L } → filter p →  filter q  → filter (p ∩ q)
-
-Filter-is-F : {L : HOD} → (f : Filter L ) → F-Filter HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
-Filter-is-F {L} f = record {
-       filter = λ x → Lift (suc n) ((filter f) ∋ x)
-     ; f⊆P = λ x f∋x →  power→⊆ _ _ (incl ( f⊆PL f  ) (lower f∋x ))
-     ; filter1 = λ {p} {q} q⊆L f∋p  p⊆q → lift ( filter1 f (q⊆L q refl-⊆) (lower f∋p) p⊆q)
-     ; filter2 = λ {p} {q} f∋p f∋q  → lift ( filter2 f (lower f∋p) (lower f∋q)) 
-    }
-
-record F-Dense {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
-   field
-       dense : L → Set n
-       d⊆P :  PL dense 
-       dense-f : L → L 
-       dense-d :  { p : L} → PL (λ x → p ⊆ x ) → dense ( dense-f p  )
-       dense-p :  { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p) 
-
-Dense-is-F : {L : HOD} → (f : Dense L ) → F-Dense HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
-Dense-is-F {L} f = record {
-       dense =  λ x → Lift (suc n) ((dense f) ∋ x)
-    ;  d⊆P = λ x f∋x →  power→⊆ _ _ (incl ( d⊆P f  ) (lower f∋x ))
-    ;  dense-f = λ x → dense-f f x
-    ;  dense-d = λ {p} d → lift ( dense-d f (d p refl-⊆ ) )
-    ;  dense-p = λ {p} d → dense-p f (d p refl-⊆) 
-  } where open Dense
-
-       
 record GenericFilter (P : HOD) : Set (suc n) where
     field
        genf : Filter P
        generic : (D : Dense P ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
 
-record F-GenericFilter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
-    field
-       GFilter : F-Filter L PL _⊆_ _∩_
-       Intersection : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → F-Dense.dense D x →  L
-       Generic : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → ( y : F-Dense.dense D x) →  F-Filter.filter GFilter (Intersection D y )
-

--- a/src/generic-filter.agda	Tue Mar 01 15:33:05 2022 +0900
+++ b/src/generic-filter.agda	Fri Mar 04 19:04:08 2022 +0900
@@ -88,9 +88,16 @@
 
 B :  (P : HOD ) (C : CountableModel P)  (i : Nat) → (x : HOD) →  o∅ o< & x   → BR
 B P C Zero x lt = record { b = x ; b>0 = lt }
-B P C (Suc i) x lt with is-o∅ ( & (BR.b (B P C i x lt) ∩ A i P C ) )
-... | no _ =  record { b = BR.b (B P C i x lt ) ∩ A i P C  ; b>0 = {!!} }
-... | yes y = record { b = BR.b (B P C i x lt) ＼ {!!} ; b>0 = {!!} }
+B P C (Suc i) x lt with is-o∅ (& (A i P C ))
+... | yes _ = B P C i x lt
+... | no _  with is-o∅ ( & (BR.b (B P C i x lt) ∩ A i P C ) )
+... | no ne =  record { b = BR.b (B P C i x lt ) ∩ A i P C  ; b>0 = ¬≡o∅< ne } 
+... | yes y = record { b = BR.b (B P C i x lt) ＼ (ODC.minimal O _ (b02 (b01 ? y ))) ; b>0 = {!!} } where
+    b02 : {x : HOD} → o∅ o< & x → ¬ ( x =h= od∅ )
+    b02 = {!!}
+    b01 : {an bn : HOD} → o∅ o< & bn  →  &( an ∩ bn ) ≡ o∅  → o∅ o< &( bn ＼ an )
+    b01 = {!!}
+       
 
 B⊆ : (P : HOD ) (C : CountableModel P)  (i : Nat) → (x : HOD) →  (lt : o∅ o< & x) → BR.b (B P C (Suc i) x lt) ⊆  BR.b (B P C (Suc i) x lt)
 B⊆ = {!!}