--- a/generic-filter.agda	Thu Aug 06 11:50:35 2020 +0900
+++ b/generic-filter.agda	Sat Aug 08 18:14:14 2020 +0900
@@ -185,16 +185,16 @@
 --
 PGHOD :  (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD
 PGHOD i C P p = record { od = record { def = λ x  →
-       odef P x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* p) y →  odef (* x) y ) }
-   ; odmax = odmax P  ; <odmax = λ {y} lt → <odmax P (proj1 lt) }  
+       odef (Power P) x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* p) y →  odef (* x) y ) }
+   ; odmax = odmax (Power P)  ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) }  
 
 ---
 --   p(n+1) = if PGHOD n qn otherwise p(n)
 --
 next-p :  (C : CountableOrdinal) (P : HOD ) (i : Nat) → (p : Ordinal) → Ordinal
-next-p C P i p with ODC.decp O ( PGHOD i C P p =h= od∅ )
+next-p C P i p with is-o∅  ( & (PGHOD i C P p))  
 next-p C P i p | yes y = p
-next-p C P i p | no not = & (ODC.minimal O (PGHOD i C P p ) not)
+next-p C P i p | no not = & (ODC.minimal O (PGHOD i C P p ) (λ eq → not (=od∅→≡o∅ eq)))  -- axiom of choice
 
 ---
 --  ascendant search on p(n)
@@ -210,7 +210,7 @@
    field
        gr : Nat
        pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p C P gr o∅)) y
-       px∈ω  : odef (Power P) x
+       x∈PP  : odef (Power P) x
 
 open PDN
 
@@ -219,7 +219,7 @@
 --
 PDHOD :  (C : CountableOrdinal) → (P : HOD ) → HOD
 PDHOD C P = record { od = record { def = λ x →  PDN C P x }
-    ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.px∈ω lt)  } where
+    ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt)  } where
 
 open PDN
 
@@ -230,17 +230,18 @@
 --  p (suc n) = if ∃ q ∈ * ( ctl→ n ) ∧ p n ⊆ q → q  (axiom of choice)
 ---             else p n
 
+P∅ : {P : HOD} → odef (Power P) o∅
+P∅ {P} =  subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅  o∅≡od∅) where
+    lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅)
+    lemma x eq = power← P od∅  (λ {x} lt → ⊥-elim (¬x<0 lt ))
+x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
+x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt
+
 P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P
 P-GenericFilter C P = record {
       genf = record { filter = PDHOD C P ; f⊆PL =  f⊆PL ; filter1 = {!!} ; filter2 = {!!} }
     ; generic = λ D → {!!}
    } where
-        P∅ : {P : HOD} → odef (Power P) o∅
-        P∅ {P} =  subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅  o∅≡od∅) where
-            lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅)
-            lemma x eq = power← P od∅  (λ {x} lt → ⊥-elim (¬x<0 lt ))
-        x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
-        x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt
         find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal)  → odef (Power P) x → odef (* (find-p C P i x)) y → odef P y 
         find-p-⊆P C P Zero x y Px Py = subst (λ k → odef P k ) &iso
             ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P)  Px)) (x<y→∋ Py))
@@ -274,7 +275,8 @@
 --
 --   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
 --
+--   W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) |  { i ∈ Nat → p i ≠ i1 } is finite }
+--
 
 
 
-