# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1645865070 -32400
# Node ID fdcbf23ba2f9ef790280407e0f1fb51d4b693929
# Parent  50949196aa88445ac5f3b9cd8bae44b3519e17bb
...

diff -r 50949196aa88 -r fdcbf23ba2f9 src/generic-filter.agda
--- a/src/generic-filter.agda	Fri Feb 25 14:46:43 2022 +0900
+++ b/src/generic-filter.agda	Sat Feb 26 17:44:30 2022 +0900
@@ -129,22 +129,22 @@
 open _⊆_
 
 find-an :{P p : HOD} → (C : CountableModel P ) → odef (Power P) (& p) → Nat
-find-an = ?
+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 = ?
+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) }
+⊆-reduction : { ψ : (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 = ?
+⊆-reduction {ψ} p ψp next ind = TransFinite {λ x → {!!} } {!!} o∅
 
 
 P-GenericFilter : (P p0 : HOD ) → (C : CountableModel P) → GenericFilter P
@@ -242,7 +242,7 @@
     →  HOD
 val x G = TransFinite {λ x → HOD } ind (& x) where
   ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD
-  ind x valy = {!!}
+  ind x valy = record { od = record { def = λ y → valS x y (& (filter (genf G))) } ; odmax = {!!} ; <odmax = {!!} }
 
 
 --