# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595650349 -32400
# Node ID cb183674facfd1f25ede6f1634ac37087aa61163
# Parent  19687f3304c9f2d07d2fb6c286e16dcf07048db1
...

diff -r 19687f3304c9 -r cb183674facf generic-filter.agda
--- a/generic-filter.agda	Sat Jul 25 12:54:28 2020 +0900
+++ b/generic-filter.agda	Sat Jul 25 13:12:29 2020 +0900
@@ -173,14 +173,14 @@
 open CountableOrdinal 
 open CountableHOD
 
-PGHOD : (P : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD
-PGHOD P 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 ) }
+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)}  
 
 next-p : (P : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → Ordinal
-next-p P i C p with ODC.decp O ( PGHOD P i C p =h= od∅ )
+next-p P i C p with ODC.decp O ( PGHOD i C p =h= od∅ )
 next-p P i C p | yes y = p
-next-p P i C p | no not = od→ord (ODC.minimal O (PGHOD P i C p ) not)
+next-p P i C p | no not = od→ord (ODC.minimal O (PGHOD i C p ) not)
 
 data PD (P : CountableHOD ) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) →  Set n where
     pd0 : PD P C o∅ 0 
@@ -202,16 +202,19 @@
 --  p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q 
 ---             else p n
 
-Gω2r :  (x : Ordinal) → (lt : infinite ∋ ord→od x ) →  Hω2 (ω→nat (ord→od x) lt ) x
-Gω2r  x = subst (λ k → (lt : odef infinite (od→ord (ord→od x))) →  Hω2 (ω→nat (ord→od x) lt ) k ) diso ( ε-induction {ψ} {!!} (ord→od x)) where
-    ψ : HOD  → Set n
-    ψ y = (lt : odef infinite (od→ord y) ) →  Hω2 (ω→nat y lt ) (od→ord y )
-    ind : {x : HOD} → ({y : HOD} → OD.def (od x) (od→ord y) →
-         (lt : infinite-d (od→ord y)) → Hω2 (ω→nat y lt) (od→ord y)) →
-         (lt : infinite-d (od→ord x)) → Hω2 (ω→nat x lt) (od→ord x)
-    ind {x} prev lt with ω→nat x lt
-    ... | Zero = subst (λ k → Hω2 Zero k) ? hφ
-    ... | Suc t = {!!}
+ψ : HOD  → Set n
+ψ y = (lt : odef infinite (od→ord y) ) →  Hω2 (ω→nat y lt ) (od→ord y )
+ind : (C : CountableOrdinal) → {x : HOD} → ({y : HOD} → OD.def (od x) (od→ord y) →
+   (lt : infinite-d (od→ord y)) → Hω2 (ω→nat y lt) (od→ord y)) →
+   (lt : infinite-d (od→ord x)) → Hω2 (ω→nat x lt) (od→ord x)
+ind C {x} prev lt with ω→nat x lt
+... | Zero = subst (λ k → Hω2 Zero k) {!!} hφ
+... | Suc i with ODC.decp O ( PGHOD i C {!!} =h= od∅ ) | prev {{!!}} {!!} {!!}
+ind C {x} prev lt | Suc i | yes p | s1 = he ?
+ind C {x} prev lt | Suc i | no ¬p | s1 = {!!}
+
+Gω2r :  (C : CountableOrdinal) → (x : Ordinal) → (lt : infinite ∋ ord→od x ) →  Hω2 (ω→nat (ord→od x) lt ) x
+Gω2r C x = subst (λ k → (lt : odef infinite (od→ord (ord→od x))) →  Hω2 (ω→nat (ord→od x) lt ) k ) diso ( ε-induction {ψ} (ind C) (ord→od x)) 
 
 P-GenericFilter : {P : CountableHOD } → (C : CountableOrdinal) → GenericFilter (phod P)
 P-GenericFilter {P} C = record {