--- a/src/generic-filter.agda	Tue Feb 22 23:37:07 2022 +0900
+++ b/src/generic-filter.agda	Fri Feb 25 14:46:43 2022 +0900
@@ -62,7 +62,7 @@
        is-Model : (x : Nat) → ctl→ x o< ctl-M
        ctl-iso→ : { x : Ordinal } → (lt : x o< ctl-M)  → ctl→ (ctl← x lt ) ≡ x 
        ctl-iso← : { x : Nat }  →  ctl← (ctl→ x ) (is-Model x)  ≡ x
-       ctl-P⊆M : Power P ⊆ * ctl-M
+       ctl-P∈M : Power P ∈ * ctl-M
 
 -- we expect ¬ G ∈ * ctl-M, so  ¬ P ∈ * ctl-M
 
@@ -128,6 +128,25 @@
 
 open _⊆_
 
+find-an :{P p : HOD} → (C : CountableModel P ) → odef (Power P) (& p) → Nat
+find-an = ?
+
+found-an :{P p : HOD} → (C : CountableModel P ) → (pw : odef (Power P) (& p)) → * (ctl→ C (find-an C pw)) =h= p
+found-an = ?
+
+record ⊆-reduce ( p :  HOD ) : Set (suc n) where
+   field
+     next : HOD
+     is-small :  next ⊆ p ∧ ( ¬ ( next =h= p ))
+
+⊆-induction : { ψ : (x : HOD) → Set (suc n) }
+    → (p : HOD) → ψ p
+    → (next : (x : HOD) → ψ x → ⊆-reduce x ) 
+    → (ind  : (x : HOD) → (m : ψ x) → ψ ( ⊆-reduce.next (next x m )) )
+    → ψ od∅
+⊆-induction = ?
+
+
 P-GenericFilter : (P p0 : HOD ) → (C : CountableModel P) → GenericFilter P
 P-GenericFilter P p0 C = record {
       genf = record { filter = PDHOD P p0 C ; f⊆PL =  f⊆PL ; filter1 = f1 ; filter2 = f2 }
@@ -152,8 +171,9 @@
              find-p-⊆P (gr lt) {!!} (& y) {!!} (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }
         f1 : {p q : HOD} → q ⊆ P → PDHOD P p0 C ∋ p → p ⊆ q → PDHOD P p0 C ∋ q
         f1 {p} {q}  q⊆P PD∋p p⊆q =  record { gr = {!!} ;  pn<gr = {!!} ; x∈PP = {!!} }  where
-           --  ¬ p ⊆ a n ⊆ p m
-           --  a(n) ∈ M, ¬ (∃ q ∈ a(n) ∧ p(n) ⊆ q ) ∨ (∃ q ∈ a(n) ∧ p(n) ⊆ q )
+           --  reduction : {ψ : (x : HOD) → x =h= od∅ → P x} → 
+           --  q ∈ a(∃ n) ⊆ P → ( p n ⊆ q →  PDHOD P p0 C ∋ q )
+           --                 ∨ (¬ (p n ⊆ q) → induction on (p n - q) 
            PDNp :  {!!} -- PD⊆⊆N P C (& p)
            PDNp = PD∋p
            f02 : {x : Ordinal} → odef q x → odef P x