Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 439:fdcbf23ba2f9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 26 Feb 2022 17:44:30 +0900
parents 50949196aa88
children d1c9f5ae5d0a
files src/generic-filter.agda
diffstat 1 files changed, 5 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- 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 = {!!} }
 
 
 --