# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564357276 -32400
# Node ID 0b9645a655426c21925e5e74815410f5f45e02b1
# Parent  38ecc75d93ceb33b9ad762e79d9fe52e00a210a7
...

diff -r 38ecc75d93ce -r 0b9645a65542 OD.agda
--- a/OD.agda	Sun Jul 28 14:50:56 2019 +0900
+++ b/OD.agda	Mon Jul 29 08:41:16 2019 +0900
@@ -500,14 +500,6 @@
          choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 
          choice X {A} X∋A not = x∋minimul A not
 
-         choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → ¬ ( X == od∅ ) → OD {suc n}
-         choice-func' X ∋-p not = lemma o∅  {!!} {!!} where
-             lemma : (ox : Ordinal {suc n} ) → ( ox o< osuc (od→ord X) ) → ((oy : Ordinal ) → oy o< ox → ¬ ( X ∋ ord→od oy ) )  → OD {suc n}
-             lemma ox lt l∅ with ∋-p X (ord→od ox)
-             lemma ox lt l∅ | yes p = ord→od ox
-             lemma ox (case1 x) l∅ | no ¬p = lemma (record { lv = Suc (lv ox); ord = Φ (Suc (lv ox))}) (case1 {!!}) {!!}
-             lemma ox (case2 x) l∅ | no ¬p = lemma (record { lv = lv ox; ord = OSuc (lv ox) (ord ox)}) {!!} {!!}
-
          --
          -- another form of regularity 
          --
@@ -566,3 +558,19 @@
                                lx ≡ ly → ly ≡ lv (od→ord z)  → ψ z 
                           lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl)
 
+         choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → ¬ ( X == od∅ ) → OD {suc n}
+         choice-func' X ∋-p not = c
+           where
+             ψ :  (y : OD {suc n} ) →  Set (suc (suc n))
+             ψ y =  OD {suc n} 
+             lemma : ( x : OD {suc n} )  →  ({ y : OD {suc n} } →  x ∋ y → ψ y)   → ψ x
+             lemma x prev = lemma1 (od→ord X) <-osuc  where
+                 lemma1 : (ox : Ordinal {suc n}) → ox o< osuc (od→ord X)  → OD {suc n}
+                 lemma1 ox lt with ∋-p X (ord→od ox)
+                 lemma1 ox lt | yes p = ord→od ox
+                 lemma1 record { lv = Zero ; ord = (Φ .0) } lt | no ¬p = {!!}
+                 lemma1 record { lv = Zero ; ord = (OSuc .0 ord₁) } lt | no ¬p = lemma1 record { lv = Zero ; ord = ord₁ } {!!} 
+                 lemma1 record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } lt | no ¬p = {!!}
+                 lemma1 record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } lt | no ¬p = lemma1 record { lv = Suc lv₁ ; ord = ord₁ } {!!} 
+             c : OD {suc n}
+             c = ε-induction (λ {x} → lemma x) X
diff -r 38ecc75d93ce -r 0b9645a65542 filter.agda
--- a/filter.agda	Sun Jul 28 14:50:56 2019 +0900
+++ b/filter.agda	Mon Jul 29 08:41:16 2019 +0900
@@ -1,9 +1,9 @@
 open import Level
-module filter where
-
+open import OD
 open import zf
 open import ordinal
-open import OD
+module filter ( n : Level )  where
+
 open import Relation.Nullary
 open import Relation.Binary
 open import Data.Empty
@@ -12,6 +12,8 @@
 open import  Relation.Binary.PropositionalEquality
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 
+od = OD→ZF {n}
+
 
 record Filter {n : Level} ( P max : OD {suc n} )  : Set (suc (suc n)) where
    field