--- a/src/generic-filter.agda	Sun Mar 13 19:22:12 2022 +0900
+++ b/src/generic-filter.agda	Mon Mar 14 17:51:16 2022 +0900
@@ -68,7 +68,6 @@
 -- find-p contains ∃ x : Ordinal → x o< & M → ∀ r ∈ M → ∈ Ord x
 -- 
 
-
 -- we expect  P ∈ * ctl-M ∧ G  ⊆ Power P  , ¬ G ∈ * ctl-M, 
 
 open CountableModel 
@@ -92,7 +91,7 @@
 ... | no not  = & (ODC.minimal O ( PGHOD i P C (find-p P C i x)) (λ eq → not (=od∅→≡o∅ eq)))  -- axiom of choice
 
 ---
--- G = { r ∈ Power P | ∃ n → p(n) ⊆ q }
+-- G = { r ∈ Power P | ∃ n → p(n) ⊆ r }
 --
 record PDN  (P p : HOD ) (C : CountableModel P)  (x : Ordinal) : Set n where
    field
@@ -168,7 +167,6 @@
                f5 : odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (find-p P C (gr PD∋q) (& p0))) y
                f5 lt = subst (λ k → odef (* (find-p P C (gr PD∋q) (& p0))) k ) &iso ( incl (p-monotonic P p0 C {gr PD∋p} {gr PD∋q} (<to≤ a))
                    (subst (λ k → odef (* (find-p P C (gr PD∋p) (& p0))) k ) (sym &iso) lt) )
---    subst (λ k → odef k y) *iso (pn<gr PD∋q y (subst (λ k → odef _ k ) &iso (incl (p-monotonic _ _ C a ) (subst (λ k → odef _ k) &iso lt) ))) ⟫
         ... | tri≈ ¬a refl ¬c = record { gr = gr PD∋p ;  pn<gr =  λ y lt → subst (λ k → odef k y ) (sym *iso) (f4 y lt);  x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q)   }  where
             f4 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (p ∩ q) y
             f4 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫ 
@@ -181,39 +179,68 @@
         fdense : (D : Dense P ) → ¬ (filter.Dense.dense D ∩ PDHOD P p0 C) ≡ od∅
         fdense D eq0  = ⊥-elim (  ∅< {Dense.dense D ∩ PDHOD P p0 C} fd01 (≡od∅→=od∅ eq0 )) where
            open Dense
+           p0⊆P : p0 ⊆ P
+           p0⊆P = ODC.power→⊆ O _ _ Pp0
            fd : HOD
-           fd = dense-f D p0
+           fd = dense-f D p0⊆P
            PP∋D : dense D ⊆ Power P
            PP∋D = d⊆P D
            fd00 : PDHOD P p0 C ∋ p0
            fd00 = record { gr = 0 ; pn<gr = λ y lt → lt ; x∈PP = Pp0 }
-           fd02 : dense D ∋ dense-f D p0 
-           fd02 = dense-d D (ODC.power→⊆ O _ _ Pp0 )
-           fd04 : dense-f D p0 ⊆ P
+           fd02 : dense D ∋ dense-f D p0⊆P
+           fd02 = dense-d D p0⊆P
+           fd04 : dense-f D p0⊆P ⊆ P
            fd04 = ODC.power→⊆ O _ _ ( incl PP∋D fd02 )
-           fd03 : PDHOD P p0 C  ∋ dense-f D p0 
-           fd03 = f1 {p0} {dense-f D p0} fd04 fd00 ( dense-p D (ODC.power→⊆ O _ _ Pp0 ) )
+           fd03 : PDHOD P p0 C  ∋ dense-f D p0⊆P
+           fd03 = f1 {p0} {dense-f D p0⊆P} fd04 fd00 ( dense-p D (ODC.power→⊆ O _ _ Pp0 ) )
            fd01 : (dense D ∩ PDHOD P p0 C) ∋ fd
            fd01 = ⟪ fd02 , fd03 ⟫ 
 
-
-
-
 open GenericFilter
 open Filter
 
-record Incompatible  (P : HOD ) : Set (suc (suc n)) where
+record Incompatible  (P p : HOD ) (PP∋p : p  ⊆ P ) : Set (suc (suc n)) where
    field
-      q : {p : HOD } → Power P ∋ p → HOD 
-      r : {p : HOD } → Power P ∋ p → HOD 
-      incompatible : { p : HOD } →  (P∋p : Power P ∋ p)  →  Power P ∋ q P∋p  →  Power P ∋ r P∋p
-          → ( p ⊆ q P∋p)   ∧ ( p ⊆ r P∋p)  
-          → ∀ ( s : HOD ) →  Power P ∋ s → ¬ (( q P∋p  ⊆ s  ) ∧ ( r P∋p  ⊆ s ))
+      q r : HOD
+      PP∋q : q ⊆ P 
+      PP∋r : r ⊆ P 
+      p⊆q :  p ⊆ q 
+      p⊆r :  p ⊆ r 
+      incompatible : ∀ ( s : HOD ) → s ⊆ P → (¬ ( q ⊆ s  )) ∨ (¬ ( r ⊆ s ))
 
 lemma725 : (P p : HOD ) (C : CountableModel P) 
-    →  * (ctl-M C) ∋ Power P
-    →  Incompatible P → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter P p {!!} C )))
-lemma725 = {!!}
+    →  (pp0 : Power P ∋ p )
+    →  * (ctl-M C) ∋ (Power P ∩  * (ctl-M C))                -- M is a Model of ZF
+    →  * (ctl-M C) ∋ ( (Power P ∩  * (ctl-M C))  ＼ filter ( genf ( P-GenericFilter P p pp0 C)) )      -- M ∋ G and M is a Model of ZF 
+    →  ((p : HOD) → (PP∋p : p  ⊆ P ) → Incompatible P p PP∋p )
+    → ¬ ( * (ctl-M C) ∋ filter ( genf ( P-GenericFilter P p pp0 C )))
+lemma725 P p C PP∋p M∋PM M∋D I M∋G = D∩G≠∅ D∩G=∅ where
+    G = filter ( genf ( P-GenericFilter P p PP∋p C ))
+    M = * (ctl-M C)
+    D : HOD
+    D = Power P ＼ G
+    p⊆P : p ⊆ P
+    p⊆P =  ODC.power→⊆ O _ _ PP∋p
+    df : {x : HOD} → x ⊆ P → HOD
+    df {x} PP∋x with Incompatible.incompatible (I p p⊆P) x PP∋x
+    ... | case1 q = Incompatible.q (I p p⊆P) 
+    ... | case2 r = Incompatible.r (I p p⊆P) 
+    df-d : {x : HOD} → (lt : x ⊆ P) → D ∋ df lt
+    df-d = {!!}
+    df-p : {x : HOD} → (lt : x ⊆ P) → x ⊆ df lt
+    df-p = {!!}
+    D-Dense : Dense P
+    D-Dense = record {
+           dense = D
+       ;   d⊆P = record { incl = λ {x} lt → proj1 lt }
+       ;   dense-f = df
+       ;   dense-d = df-d
+       ;   dense-p = df-p
+     }
+    D∩G=∅ : ( D ∩ G ) =h= od∅ 
+    D∩G=∅ = {!!}
+    D∩G≠∅ : ¬ (( D ∩ G ) =h= od∅ )
+    D∩G≠∅ eq = generic (P-GenericFilter P p PP∋p C) D-Dense ( ==→o≡ eq )
 
 open import PFOD O
 
@@ -222,11 +249,11 @@
 -- ω→2 : HOD
 -- ω→2 = Power infinite
 
-lemma725-1 :   Incompatible HODω2
+lemma725-1 :  (p : HOD) → (PP∋p : p  ⊆ HODω2 ) → Incompatible HODω2 p PP∋p
 lemma725-1 = {!!}
 
 lemma726 :  (C : CountableModel HODω2) 
-    →  Union ( Replace HODω2 (λ p → filter ( genf ( P-GenericFilter HODω2 p {!!} C )))) =h= ω→2
+    →  Union ( Replace' (Power HODω2) (λ p lt → filter ( genf ( P-GenericFilter HODω2 p lt C )))) =h= ω→2 -- HODω2 ∋ p
 lemma726 = {!!}
 
 --