# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595663122 -32400
# Node ID e98b5774d1801bba0772d5f0062e92c5a7619f46
# Parent  d58edc4133b01069c362e92111776fc3698c4198
generic filter defined

diff -r d58edc4133b0 -r e98b5774d180 generic-filter.agda
--- a/generic-filter.agda	Sat Jul 25 13:33:53 2020 +0900
+++ b/generic-filter.agda	Sat Jul 25 16:45:22 2020 +0900
@@ -173,40 +173,38 @@
 open CountableOrdinal 
 open CountableHOD
 
-PGHOD :  (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD
-PGHOD i C p = record { od = record { def = λ x → odef (ord→od (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (ord→od p) y →  odef (ord→od x) y ) }
-   ; odmax = ctl→ C i  ; <odmax = λ {y} lt → odefo→o< (proj1 lt)}  
+PGHOD :  (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD
+PGHOD i C P p = record { od = record { def = λ x  → odef P x ∧ odef (ord→od (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (ord→od p) y →  odef (ord→od x) y ) }
+   ; odmax = odmax P  ; <odmax = λ {y} lt → <odmax P (proj1 lt) }  
 
-next-p : (M : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → Ordinal
-next-p M i C p with ODC.decp O ( PGHOD i C p =h= od∅ )
-next-p M i C p | yes y = p
-next-p M i C p | no not = od→ord (ODC.minimal O (PGHOD i C p ) not)
+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 | yes y = p
+next-p C P i p | no not = od→ord (ODC.minimal O (PGHOD i C P p ) not)
 
-data PD (M : CountableHOD ) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) →  Set n where
-    pd0 : PD M C o∅ 0 
-    pdsuc : {p : Ordinal } {i : Nat} → PD M C p i  → PD M C (next-p M i C p) (Suc i) 
+find-p :  (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x : Ordinal) → Ordinal
+find-p C P Zero x = x
+find-p C P (Suc i) x = find-p C P i ( next-p C P i x )
 
-record PDN (M : CountableHOD ) (C : CountableOrdinal) (x : Ordinal) : Set n where
+record PDN  (C : CountableOrdinal) (P : HOD ) (x : Ordinal) : Set n where
    field
-       gr : Ordinal
-       pn<gr : (y : Ordinal) → odef (ord→od x) y → odef (ord→od gr) y
-       px∈ω  : odef (mhod M) x
-       grx∈ω : odef (mhod M) gr
-       pdod : PD M C x (mtl← M gr grx∈ω)
+       gr : Nat
+       pn<gr : (y : Ordinal) → odef (ord→od x) y → odef (ord→od (find-p C P gr o∅)) y
+       px∈ω  : odef P x
 
 open PDN
 
-PDHOD : (M : CountableHOD ) → (C : CountableOrdinal) → HOD
-PDHOD M C = record { od = record { def = λ x →  PDN M C x }
-    ; odmax = odmax (mhod M) ; <odmax = λ {y} lt → ordtrans (<odmax (mhod M) (px∈ω lt)) {!!}  } where
+PDHOD :  (C : CountableOrdinal) → (P : HOD ) → HOD
+PDHOD C P = record { od = record { def = λ x →  PDN C P x }
+    ; odmax = odmax (Power P) ; <odmax = {!!}  } where
 
 --
 --  p 0 ≡ ∅
 --  p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q 
 ---             else p n
 
-P-GenericFilter : {M : CountableHOD } → (C : CountableOrdinal) → GenericFilter (mhod M)
-P-GenericFilter {M} C = record {
-      genf = record { filter = PDHOD M C ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} }
+P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P
+P-GenericFilter C P = record {
+      genf = record { filter = PDHOD C P ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} }
     ; generic = λ D → {!!}
    }